Library Subsets.Subset

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Operations on subsets represented by predicates.

Description

Subsets of the type U can be defined using predicates: they are represented by belonging functions of type U Prop. This is the main API of the file.
Subsets can also be defined as the range of some function: given some index type Idx, they are represented by "enumerating functions" of type Idx U.
Most of the properties are tautologies, and can be found on Wikipedia: https://en.wikipedia.org/wiki/List_of_set_identities_and_relations

Support for unit types

  • unit_type x states that all elements of the type are equal to x;
  • is_unit_type is the predicate stating that a type has only one element;

Some properties of union and inter

  • {union,inter}_inj_{l,r} state the condition for the corresponding operator to be injective wrt its first (left) or second (right) argument.

Used logic axioms

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import ssr.

From Logic Require Import logic_compl.

Section Base_Def0a.

Context {U : Type}.
Variable A : U Prop.
Definition subset_to_Idx : {x | A x} U := proj1_sig (P := A).

Context {Idx : Type}.
Variable B : Idx U.
Definition subset_of_Idx : U Prop := fun x i, x = B i.

End Base_Def0a.

Section Subset_Def0b.

Definition unit_type {U : Type} (x : U) : Prop := y : U, y = x.
Definition is_unit_type (U : Type) : Prop := x : U, unit_type x.

Lemma unit_type_correct :
   {U : Type}, is_unit_type U (x : U), unit_type x.
Proof. moveU [x0 HU] x y; rewrite (HU x); easy. Qed.

Lemma is_unit_type_correct :
   {U : Type} (x : U), unit_type x is_unit_type U.
Proof. intros U x HU; x; auto. Qed.

End Subset_Def0b.

Section Base_Def1.

Context {U : Type}.
Nullary constructors of subsets.

Definition emptyset : U Prop := fun _False.
Definition fullset : U Prop := fun _True.

Unary constructors of subsets.
Either the emptyset when p := False, or the fullset U when p := True.
Definition Prop_cst : Prop U Prop := fun p _p.

Definition singleton : U U Prop := fun a xx = a.

Unary predicates on subsets.

Variable A : U Prop.
Definition empty : Prop := x, A x False.
Definition nonempty : Prop := x, A x.
Definition full : Prop := x, A x.

Unary operation on subsets.

Definition compl : U Prop := fun x¬ A x.

Binary predicates on subsets.

Variable B : U Prop.
Definition incl : Prop := x, A x B x.
Definition same : Prop := x, A x B x.

Definition disj : Prop := x, A x B x False.

Binary operations on subsets.

Definition union : U Prop := fun xA x B x.
Definition inter : U Prop := fun xA x B x.

End Base_Def1.

Section Base_Def2.

Context {U : Type}.
Sesquary operation on subsets.

Variable A : U Prop. Variable a : U.
Definition add : U Prop := union A (singleton a).

More binary operation on subsets.

Variable B : U Prop.
Definition diff : U Prop := inter A (compl B).

Ternary predicate on subsets.

Variable C : U Prop.
Definition partition : Prop := A = union B C disj B C.

End Base_Def2.

Section Base_Def3.

Context {U : Type}.
Binary constructor of subsets.

Variable a b : U.
Definition pair : U Prop := add (singleton a) b.

More binary operation on subsets.

Variable A B : U Prop.
Definition sym_diff : U Prop := union (diff A B) (diff B A).

End Base_Def3.

Section Base_Def4.

Context {U1 U2 : Type}.
Variable A1 : U1 Prop. Variable A2 : U2 Prop.
Definition prod : U1 × U2 Prop :=
  inter (fun xA1 (fst x)) (fun xA2 (snd x)).

Definition swap_c : {U : Type}, (U1 × U2 U) U2 × U1 U :=
  fun U f xf (snd x, fst x).

End Base_Def4.

Section Prop_Facts0.

Context {U : Type}.
Correctness results.

Lemma subset_to_Idx_correct :
   (A : U Prop) x, A x i, x = subset_to_Idx A i.
Proof.
intros A x; split.
intros Hx; (exist _ x Hx); easy.
intros [[y Hy] Hx]; rewrite Hx; easy.
Qed.

Context {Idx : Type}.

Lemma subset_of_Idx_to_Idx :
   (A : U Prop) x, subset_of_Idx (subset_to_Idx A) x A x.
Proof.
intros A x; split.
intros [[y Hy] Hi]; rewrite Hi; easy.
intros Hx; (exist _ _ Hx); easy.
Qed.


Extensionality of subsets.

Lemma subset_ext : (A B : U Prop), same A B A = B.
Proof. intros; apply fun_ext; intro; now apply prop_ext. Qed.

Lemma subset_ext_equiv :
   (A B : U Prop), A = B incl A B incl B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_ext; split; [apply H1 | apply H2].
Qed.

Lemma subset_ext_contra :
   {A B : U Prop}, A B x, ¬ (A x B x).
Proof.
intros A B; rewrite contra_not_l_equiv not_ex_not_all_equiv; apply subset_ext.
Qed.

Lemma subset_ext_contra_rev :
   {A B : U Prop},
    ( x, (A x compl B x) (compl A x B x)) A B.
Proof.
intros A B;
    rewrite contra_not_r_equiv not_ex_all_not_equiv; intro; subst; intros x.
rewrite not_or_equiv !not_and_equiv NNPP_equiv; tauto.
Qed.

Lemma subset_ext_contra_equiv :
   {A B : U Prop}, A B x, ¬ (A x B x).
Proof.
intros A B; split; [apply subset_ext_contra |].
move⇒ [x /not_iff_equiv Hx]; apply subset_ext_contra_rev; x; easy.
Qed.

End Prop_Facts0.

Ltac subset_unfold :=
  repeat unfold
    partition, disj, same, incl, full, nonempty, empty,
    pair,
    swap_c, prod, sym_diff, diff, add, inter, union, compl,
    singleton, Prop_cst, fullset, emptyset.
Ltac subset_auto :=
  subset_unfold; try easy; try tauto; auto.

Ltac subset_ext_auto0 :=
  apply subset_ext; subset_auto.

Ltac subset_ext_auto1 x :=
  subset_ext_auto0; intros x; subset_auto.

Ltac subset_ext_auto2 x Hx :=
  subset_ext_auto1 x; split; intros Hx; subset_auto.

Tactic Notation "subset_ext_auto" := subset_ext_auto0.
Tactic Notation "subset_ext_auto" ident(x) := subset_ext_auto1 x.
Tactic Notation "subset_ext_auto" ident(x) ident(Hx) := subset_ext_auto2 x Hx.

Section Prop_Facts.

Context {U : Type}.
Facts about emptyset and fullset.

Lemma not_in_emptyset : (x : U), ¬ emptyset x.
Proof. easy. Qed.

Lemma not_in_empty : P (x : U), empty P ¬ P x.
Proof. intros P x HP Hx; apply (HP x Hx). Qed.

Lemma nonempty_is_not_empty :
   (A : U Prop), nonempty A ¬ empty A.
Proof.
intros A; split.
intros [x Hx] H; apply (H x); easy.
apply not_all_not_ex.
Qed.

Lemma empty_emptyset :
   (A : U Prop),
    empty A A = emptyset.
Proof.
intros; split; intros H.
subset_ext_auto x Hx; now apply (H x).
now rewrite H.
Qed.

Lemma in_fullset : (x : U), fullset x.
Proof. easy. Qed.

Lemma in_full : P (x : U), full P P x.
Proof. easy. Qed.

Lemma full_fullset :
   (A : U Prop),
    full A A = fullset.
Proof.
intros; split; intros H.
now apply subset_ext.
now rewrite H.
Qed.

Lemma full_fullset_alt : full (@fullset U).
Proof. easy. Qed.

Facts about singleton.

Lemma singleton_in : a : U, singleton a a.
Proof. subset_auto. Qed.

Lemma singleton_out : a x : U, x a compl (singleton a) x.
Proof. subset_auto. Qed.

Lemma is_singleton_equiv :
   (A : U Prop) x,
    A = singleton x nonempty A y, A y y = x.
Proof.
intros A x; split; [intros; subst; split; [ x |]; easy |].
intros [[y Hy] HA]; apply subset_ext_equiv; split; intros z Hz;
    [apply HA | rewrite Hz -(HA y)]; easy.
Qed.

Facts about incl.
It is an order binary relation.

Lemma incl_refl :
   (A B : U Prop),
    same A B incl A B.
Proof.
intros A B H x; now rewrite (H x).
Qed.

Lemma incl_antisym :
   (A B : U Prop),
    incl A B incl B A A = B.
Proof.
intros; now rewrite subset_ext_equiv.
Qed.

Lemma incl_trans :
   (A B C : U Prop),
    incl A B incl B C incl A C.
Proof.
intros; intros x Hx; auto.
Qed.

Lemma full_not_empty :
  inhabited U ¬ incl (@fullset U) emptyset.
Proof.
subset_unfold; split.
intros [x]; auto.
intros H; apply exists_inhabited with (fun x¬ (True False)).
now apply not_all_ex_not in H.
Qed.

Lemma incl_empty :
   (A : U Prop),
    incl A emptyset A = emptyset.
Proof.
intros A H; subset_ext_auto x Hx; apply (H x Hx).
Qed.

Lemma full_incl :
   (A : U Prop),
    incl fullset A A = fullset.
Proof.
intros A H; subset_ext_auto x Hx; apply (H x Hx).
Qed.

Facts about same.
It is an equivalence binary relation.

Lemma same_refl : {A B : U Prop}, A = B same A B.
Proof. intros; subst; easy. Qed.

Lemma same_sym : (A B : U Prop), same A B same B A.
Proof. easy. Qed.

Lemma same_trans :
   (A B C : U Prop), same A B same B C same A C.
Proof. intros A B C H1 H2 x; now rewrite (H1 x). Qed.

Facts about disj.

Lemma disj_equiv_def :
   (A B : U Prop),
    disj A B inter A B = emptyset.
Proof.
intros; rewrite -empty_emptyset; subset_unfold; split;
    intros H x; intros; now apply (H x).
Qed.

Lemma disj_irrefl :
   (A : U Prop),
    disj A A A = emptyset.
Proof.
intros; rewrite -empty_emptyset; split; intros H x Hx; now apply (H x).
Qed.

Lemma disj_sym :
   (A B : U Prop),
    disj A B disj B A.
Proof.
intros; split; intros H x Hx1 Hx2; now apply (H x).
Qed.

Lemma disj_full_l :
   (A : U Prop),
    disj fullset A A = emptyset.
Proof.
intros A H; apply empty_emptyset; intros x Hx; now apply (H x).
Qed.

Lemma disj_full_r :
   (A : U Prop),
    disj A fullset A = emptyset.
Proof.
intros A; rewrite disj_sym; apply disj_full_l.
Qed.

Lemma disj_monot_l :
   (A B C : U Prop),
    incl A B
    disj B C disj A C.
Proof.
intros A B C H1 H2 x Hx1 Hx2; apply (H2 x); auto.
Qed.

Lemma disj_monot_r :
   (A B C : U Prop),
    incl A B
    disj C B disj C A.
Proof.
intros A B C H1 H2 x Hx1 Hx2; apply (H2 x); auto.
Qed.

Lemma incl_disj :
   (A B : U Prop),
    incl A B
    disj A B A = emptyset.
Proof.
intros; split; intros H2.
apply empty_emptyset; intros x Hx; apply (H2 x); auto.
now rewrite H2.
Qed.

End Prop_Facts.

Section Compl_Facts.

Facts about complement.

Context {U : Type}.
Lemma compl_empty :
  compl (@emptyset U) = fullset.
Proof.
now apply subset_ext.
Qed.

Lemma compl_full :
  compl (@fullset U) = emptyset.
Proof.
subset_ext_auto.
Qed.

Lemma compl_invol :
   (A : U Prop),
    compl (compl A) = A.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma compl_monot :
   (A B : U Prop),
    incl A B incl (compl B) (compl A).
Proof.
subset_auto; intros; intuition.
Qed.

Lemma incl_compl_equiv :
   (A B : U Prop),
    incl (compl B) (compl A) incl A B.
Proof.
intros; split; [rewrite -{2}(compl_invol A) -{2}(compl_invol B) |];
    apply compl_monot.
Qed.

Lemma same_compl :
   (A B : U Prop),
    same A B same (compl A) (compl B).
Proof.
subset_unfold; intros; now apply not_iff_compat.
Qed.

Lemma same_compl_equiv :
   (A B : U Prop),
    same (compl A) (compl B) same A B.
Proof.
intros; split; [rewrite -{2}(compl_invol A) -{2}(compl_invol B) |];
    apply same_compl.
Qed.

Lemma compl_reg :
   (A B : U Prop),
    same (compl A) (compl B) A = B.
Proof.
intros; now apply subset_ext, same_compl_equiv.
Qed.

Lemma compl_ext :
   (A B : U Prop),
    compl A = compl B A = B.
Proof.
intros A B H; apply compl_reg; now rewrite H.
Qed.

Lemma disj_incl_compl_l :
   (A B : U Prop),
    disj A B incl A (compl B).
Proof.
subset_auto.
Qed.

Lemma disj_incl_compl_r :
   (A B : U Prop),
    disj A B incl B (compl A).
Proof.
intros A B; rewrite disj_sym; apply disj_incl_compl_l.
Qed.

End Compl_Facts.

Section Union_Facts.

Facts about union.

Context {U : Type}.
Lemma union_assoc :
   (A B C : U Prop),
    union (union A B) C = union A (union B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_comm :
   (A B : U Prop),
    union A B = union B A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_idem :
   (A : U Prop),
    union A A = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_empty_l :
   (A : U Prop),
    union emptyset A = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_empty_r :
   (A : U Prop),
    union A emptyset = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_empty :
   (A B : U Prop),
    union A B = emptyset A = emptyset B = emptyset.
Proof.
intros; do 3 rewrite -empty_emptyset; split.
intros H; split; intros x Hx; apply (H x); [now left | now right].
intros [H1 H2] x [Hx | Hx]; [now apply (H1 x) | now apply (H2 x)].
Qed.

Lemma union_full_l :
   (A : U Prop),
    union fullset A = fullset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_full_r :
   (A : U Prop),
    union A fullset = fullset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_ub_l :
   (A B : U Prop),
    incl A (union A B).
Proof.
subset_auto.
Qed.

Lemma union_ub_r :
   (A B : U Prop),
    incl B (union A B).
Proof.
subset_auto.
Qed.

Lemma union_lub :
   (A B C : U Prop),
    incl A C incl B C
    incl (union A B) C.
Proof.
intros; intros x [H3 | H3]; auto.
Qed.

Lemma incl_union :
   (A B C : U Prop),
    incl (union A B) C incl A C incl B C.
Proof.
intros A B C H; split; intros x Hx; apply (H x); [now left | now right].
Qed.

Lemma union_left : (A B : U Prop), incl A B union B A = B.
Proof.
move=>> H; apply subset_ext_equiv; split; intros x Hx;
    [destruct Hx; [| apply H] | left]; easy.
Qed.

Lemma union_left_rev : (A B : U Prop), union B A = B incl A B.
Proof. move=>> <-; apply union_ub_r. Qed.

Lemma union_left_equiv : (A B : U Prop), union B A = B incl A B.
Proof. intros; split; [apply union_left_rev | apply union_left]. Qed.

Lemma union_right : (A B : U Prop), incl A B union A B = B.
Proof. move=>>; rewrite union_comm; apply union_left. Qed.

Lemma union_right_rev : (A B : U Prop), union A B = B incl A B.
Proof. move=>>; rewrite union_comm; apply union_left_rev. Qed.

Lemma union_right_equiv : (A B : U Prop), union A B = B incl A B.
Proof. move=>>; rewrite union_comm; apply union_left_equiv. Qed.

Lemma union_monot :
   (A B C D : U Prop),
    incl A B incl C D incl (union A C) (union B D).
Proof.
intros A B C D HAB HCD x [Hx | Hx]; [left | right]; auto.
Qed.

Lemma union_monot_l :
   (A B C : U Prop),
    incl A B incl (union A C) (union B C).
Proof.
intros; apply union_monot; easy.
Qed.

Lemma union_monot_r :
   (A B C : U Prop),
    incl A B incl (union C A) (union C B).
Proof.
intros; apply union_monot; easy.
Qed.

Lemma union_inj_l :
   (B : U Prop) {A1 A2},
    incl B (compl A1) incl B (compl A2)
    union A1 B = union A2 B A1 = A2.
Proof.
intros B A1 A2 HA1 HA2 HA; apply subset_ext_equiv; split; intros x Hx.
move: (union_ub_l A1 B x Hx); rewrite HA; move⇒ [| /HA1]; easy.
move: (union_ub_l A2 B x Hx); rewrite -HA; move⇒ [| /HA2]; easy.
Qed.

Lemma union_inj_r :
   (A : U Prop) {B1 B2},
    incl A (compl B1) incl A (compl B2)
    union A B1 = union A B2 B1 = B2.
Proof. intros A B1 B2; rewrite !(union_comm A); apply union_inj_l. Qed.

Lemma disj_union_l :
   (A B C : U Prop),
    disj (union A B) C disj A C disj B C.
Proof.
intros; split.
intros H; split; intros x Hx1 Hx2; apply (H x); try easy; [now left | now right].
intros [H1 H2] x [Hx1 | Hx1] Hx2; [now apply (H1 x) | now apply (H2 x)].
Qed.

Lemma disj_union_r :
   (A B C : U Prop),
    disj A (union B C) disj A B disj A C.
Proof.
intros A B C; now rewrite disj_sym disj_union_l (disj_sym B) (disj_sym C).
Qed.

Lemma union_compl_l :
   (A : U Prop),
    union (compl A) A = fullset.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma union_compl_r :
   (A : U Prop),
    union A (compl A) = fullset.
Proof.
intros; subset_ext_auto x.
Qed.

End Union_Facts.

Section Inter_Facts.

Facts about intersection.

Context {U : Type}.
Lemma inter_assoc :
   (A B C : U Prop),
    inter (inter A B) C = inter A (inter B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_comm :
   (A B : U Prop),
    inter A B = inter B A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_idem :
   (A : U Prop),
    inter A A = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_singleton_l_in :
   (A : U Prop) x, A x inter (singleton x) A = singleton x.
Proof.
intros; apply subset_ext_equiv; split; intro;
    [intros [Hy _] | move⇒ ->; split]; easy.
Qed.

Lemma inter_singleton_r_in :
   (A : U Prop) x, A x inter A (singleton x) = singleton x.
Proof. intros; rewrite inter_comm; apply inter_singleton_l_in; easy. Qed.

Lemma inter_singleton_l_out :
   (A : U Prop) x, compl A x inter (singleton x) A = emptyset.
Proof.
intros; apply subset_ext_equiv; split; intro; [intros [-> Hy] |]; easy.
Qed.

Lemma inter_singleton_r_out :
   (A : U Prop) x, compl A x inter A (singleton x) = emptyset.
Proof. intros; rewrite inter_comm; apply inter_singleton_l_out; easy. Qed.

Lemma inter_full_l :
   (A : U Prop),
    inter fullset A = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_full_r :
   (A : U Prop),
    inter A fullset = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_full :
   (A B : U Prop),
    inter A B = fullset A = fullset B = fullset.
Proof.
intros; do 3 rewrite -full_fullset; split.
intros H; split; intros x; now destruct (H x).
intros [H1 H2] x; split; [apply (H1 x) | apply (H2 x)].
Qed.

Lemma inter_empty_l :
   (A : U Prop),
    inter emptyset A = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_empty_r :
   (A : U Prop),
    inter A emptyset = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_lb_l :
   (A B : U Prop),
    incl (inter A B) A.
Proof.
subset_auto.
Qed.

Lemma inter_lb_r :
   (A B : U Prop),
    incl (inter A B) B.
Proof.
subset_auto.
Qed.

Lemma inter_glb :
   (A B C : U Prop),
    incl C A incl C B
    incl C (inter A B).
Proof.
intros; intros x Hx; split; auto.
Qed.

Lemma incl_inter :
   (A B C : U Prop),
    incl A (inter B C) incl A B incl A C.
Proof.
intros A B C H; split; intros x Hx; now apply (H x).
Qed.

Lemma inter_left :
   (A B : U Prop),
    incl A B inter A B = A.
Proof.
intros; split.
rewrite subset_ext_equiv; split; intros x.
intros [Hx1 Hx2]; auto.
intros Hx; split; auto.
intros H x Hx; rewrite -H in Hx; now destruct Hx as [_ Hx].
Qed.

Lemma inter_right :
   (A B : U Prop),
    incl B A inter A B = B.
Proof.
intros; rewrite inter_comm; apply inter_left.
Qed.

Lemma inter_monot :
   (A B C D : U Prop),
    incl A B incl C D incl (inter A C) (inter B D).
Proof.
intros A B C D HAB HCD x [Hx1 Hx2]; split; auto.
Qed.

Lemma inter_monot_l :
   (A B C : U Prop),
    incl A B incl (inter A C) (inter B C).
Proof.
intros; apply inter_monot; easy.
Qed.

Lemma inter_monot_r :
   (A B C : U Prop),
    incl A B incl (inter C A) (inter C B).
Proof.
intros; apply inter_monot; easy.
Qed.

Lemma inter_disj_compat_l :
   (A B C : U Prop),
    disj A B disj (inter C A) (inter C B).
Proof.
intros A B C; rewrite !disj_equiv_def -!empty_emptyset; intros H.
intros x [[_ Hx1] [_ Hx2]]; now apply (H x).
Qed.

Lemma inter_disj_compat_r :
   (A B C : U Prop),
    disj A B disj (inter A C) (inter B C).
Proof.
intros A B C; rewrite (inter_comm A) (inter_comm B); apply inter_disj_compat_l.
Qed.

Lemma inter_compl_l :
   (A : U Prop),
    inter (compl A) A = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_compl_r :
   (A : U Prop),
    inter A (compl A) = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_empty_l_alt :
   (A B : U Prop), incl A (compl B) inter A B = emptyset.
Proof.
intros A B H; apply subset_ext_equiv; split; [move: H | easy].
rewrite -(inter_compl_l B); apply inter_monot_l.
Qed.

Lemma inter_empty_r_alt :
   (A B : U Prop), incl B (compl A) inter A B = emptyset.
Proof. move=>>; rewrite inter_comm; apply inter_empty_l_alt. Qed.

End Inter_Facts.

Section Union_Inter_Facts.

Facts about union and intersection.

Context {U : Type}.
Lemma incl_inter_union :
   (A B : U Prop),
    incl (inter A B) (union A B).
Proof.
intros; intros x [Hx _]; now left.
Qed.

Lemma disj_inter_union :
   (A B : U Prop),
    disj (inter A B) (union A B) disj A B.
Proof.
intros; split; intros H x.
intros Hx1 Hx2; apply (H x); [easy | now left].
intros [Hx1 Hx2] _; now apply (H x).
Qed.

De Morgan's laws.

Lemma compl_union :
   (A B : U Prop),
    compl (union A B) = inter (compl A) (compl B).
Proof.
intros; subset_ext_auto.
Qed.

Lemma compl_inter :
   (A B : U Prop),
    compl (inter A B) = union (compl A) (compl B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma inter_inj_l :
   (B : U Prop ){A1 A2},
    incl A1 B incl A2 B
    inter (compl A1) B = inter (compl A2) B A1 = A2.
Proof.
moveB A1 A2 /compl_monot HA1 /compl_monot HA2 /(f_equal compl).
rewrite !compl_inter !compl_invol; intros HA.
apply compl_reg; rewrite (union_inj_l _ HA1 HA2 HA); easy.
Qed.

Lemma inter_inj_r :
   (A : U Prop) {B1 B2},
    incl B1 A incl B2 A
    inter A (compl B1) = inter A (compl B2) B1 = B2.
Proof. intros A B1 B2; rewrite !(inter_comm A); apply inter_inj_l. Qed.

Distributivity.

Lemma union_union_distr_l :
   (A B C : U Prop),
    union A (union B C) = union (union A B) (union A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma union_union_distr_r :
   (A B C : U Prop),
    union (union A B) C = union (union A C) (union B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma union_inter_distr_l :
   (A B C : U Prop),
    union A (inter B C) = inter (union A B) (union A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma union_inter_distr_r :
   (A B C : U Prop),
    union (inter A B) C = inter (union A C) (union B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma union_inter :
   (A B C D : U Prop),
    union (inter A B) (inter C D) =
    inter (inter (union A C) (union B C)) (inter (union A D) (union B D)).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_union_distr_l :
   (A B C : U Prop),
    inter A (union B C) = union (inter A B) (inter A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_union_distr_r :
   (A B C : U Prop),
    inter (union A B) C = union (inter A C) (inter B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_union :
   (A B C D : U Prop),
    inter (union A B) (union C D) =
    union (union (inter A C) (inter B C)) (union (inter A D) (inter B D)).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_inter_distr_l :
   (A B C : U Prop),
    inter A (inter B C) = inter (inter A B) (inter A C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_inter_distr_r :
   (A B C : U Prop),
    inter (inter A B) C = inter (inter A C) (inter B C).
Proof.
intros; rewrite subset_ext_equiv; split; subset_auto.
Qed.

Lemma inter_union_compl_l :
   (A : U Prop) {B}, incl (inter (union A B) (compl A)) B.
Proof.
move=>>; rewrite inter_union_distr_r inter_compl_r union_empty_l.
intros [Hx _]; easy.
Qed.

Lemma inter_union_compl_r :
   {A} (B : U Prop), incl (inter (union A B) (compl B)) A.
Proof. intros; rewrite union_comm; apply inter_union_compl_l. Qed.

Lemma inter_eq_union :
   {A B : U Prop}, inter A B = union A B A = B.
Proof.
move=>> H; apply subset_ext; intro; apply and_or_equiv, (same_refl H).
Qed.

Lemma inter_union_inj_l :
   {A B : U Prop} C,
    inter A C = inter B C union A C = union B C A = B.
Proof.
intros A B C H1 H2; apply subset_ext; intro; apply and_or_inj_l with (C x);
    [apply (same_refl H1) | apply (same_refl H2)].
Qed.

Lemma inter_union_inj_r :
   A {B C : U Prop},
    inter A B = inter A C union A B = union A C B = C.
Proof.
intros A B C H1 H2; apply subset_ext; intro; apply and_or_inj_r with (A x);
    [apply (same_refl H1) | apply (same_refl H2)].
Qed.

Lemma disj_compl_l :
   (A B : U Prop),
    disj (compl A) B ¬ empty B ¬ disj A B.
Proof.
intros A B; rewrite !disj_equiv_def; intros H1 H2 H3.
contradict H2; apply empty_emptyset.
rewrite -(inter_full_l B).
rewrite -(union_compl_l A) inter_union_distr_r H1 H3.
now apply union_empty.
Qed.

Lemma disj_compl_r :
   (A B : U Prop),
    disj A (compl B) ¬ empty A ¬ disj A B.
Proof.
intros A B; rewrite 2!(disj_sym A); intros H1 H2; now apply disj_compl_l.
Qed.

End Union_Inter_Facts.

Section Add_Facts.

Facts about addition of one element.

Context {U : Type}.
Lemma incl_add_l :
   A B (a : U), incl (add A a) B incl A B B a.
Proof.
intros A B a; split; intros H.
apply incl_union in H; split; try apply H; apply singleton_in.
apply union_lub; try easy; intros x Hx; now rewrite Hx.
Qed.

Lemma incl_add_r :
   A (a : U), incl A (add A a).
Proof.
intros; apply union_ub_l.
Qed.

Lemma add_in :
   A (a : U), add A a a.
Proof.
intros; apply union_ub_r, singleton_in.
Qed.

End Add_Facts.

Section Diff_Facts.

Facts about set difference.

Context {U : Type}.
Lemma diff_equiv_def_inter :
   (A B : U Prop),
    diff A B = inter A (compl B).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_equiv_def_union :
   (A B : U Prop),
    diff A B = compl (union (compl A) B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma compl_equiv_def_diff :
   (A : U Prop),
    compl A = diff fullset A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_equiv_def_diff :
   (A B : U Prop),
    inter A B = diff A (diff A B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma union_equiv_def_diff :
   (A B : U Prop),
    union A B = compl (diff (compl A) B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_lb_l :
   (A B : U Prop),
    incl (diff A B) A.
Proof.
intros; apply inter_lb_l.
Qed.

Lemma diff_lb_r :
   (A B : U Prop),
    incl (diff A B) (compl B).
Proof.
intros; apply inter_lb_r.
Qed.

Lemma partition_union_diff_l :
   (A B : U Prop),
    partition (union A B) (diff A B) B.
Proof.
intros; split.
subset_ext_auto x.
subset_auto.
Qed.

Lemma partition_union_diff_r :
   (A B : U Prop),
    partition (union A B) A (diff B A).
Proof.
intros; split.
subset_ext_auto x.
subset_auto.
Qed.

Lemma diff_monot_l :
   (A B C : U Prop),
    incl A B incl (diff A C) (diff B C).
Proof.
intros A B C H x [Hx1 Hx2]; split; [now apply H | easy].
Qed.

Lemma diff_monot_r :
   (A B C : U Prop),
    incl B C incl (diff A C) (diff A B).
Proof.
intros A B C H x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
Qed.

Lemma diff_disj :
   (A B : U Prop),
    disj A B diff A B = A.
Proof.
intros; rewrite subset_ext_equiv; split.
intros H; split; subset_unfold; intros x Hx1; specialize (H x); intuition.
intros [_ H] x Hx1 Hx2; specialize (H x Hx1); now destruct H as [_ H].
Qed.

Lemma diff_disj_compat_r :
   (A B C : U Prop),
    disj A B disj (diff A C) (diff B C).
Proof.
intros A B C H x HAx HBx; apply (H x); now apply (diff_lb_l _ C).
Qed.

Lemma diff_empty :
   (A B : U Prop),
    diff A B = emptyset incl A B.
Proof.
intros; rewrite -empty_emptyset; split; intros H.
intros x Hx1; apply NNPP; intros Hx2; now apply (H x).
intros x [Hx1 Hx2]; auto.
Qed.

Lemma diff_empty_diag :
   (A : U Prop),
    diff A A = emptyset.
Proof.
intros; now rewrite diff_empty.
Qed.

Lemma full_diff :
   (A B : U Prop),
    diff A B = fullset A = fullset B = emptyset.
Proof.
intros; do 2 rewrite -full_fullset; rewrite -empty_emptyset.
split; intros H.
split; intros x; now destruct (H x) as [H1 H2].
intros x; destruct H as [H1 H2]; split; [apply H1 | exact (H2 x)].
Qed.

Lemma compl_diff :
   (A B : U Prop),
    compl (diff A B) = union (compl A) B.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_empty_l :
   (A : U Prop),
    diff emptyset A = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_empty_r :
   (A : U Prop),
    diff A emptyset = A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_full_l :
   (A : U Prop),
    diff fullset A = compl A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_full_r :
   (A : U Prop),
    diff A fullset = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_compl_l :
   (A B : U Prop),
    diff (compl A) B = diff (compl B) A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_compl_r :
   (A B : U Prop),
    diff A (compl B) = diff B (compl A).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_compl :
   (A B : U Prop),
    diff (compl A) (compl B) = diff B A.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_compl_l_diag : (A : U Prop), diff (compl A) A = compl A.
Proof. intros; subset_ext_auto. Qed.

Lemma diff_compl_r_diag : (A : U Prop), diff A (compl A) = A.
Proof. intros; subset_ext_auto. Qed.

Lemma diff_union_distr_l :
   (A B C : U Prop),
    diff (union A B) C = union (diff A C) (diff B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_union_distr_r :
   (A B C : U Prop),
    diff A (union B C) = inter (diff A B) (diff A C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_inter_distr_l :
   (A B C : U Prop),
    diff (inter A B) C = inter (diff A C) (diff B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_inter_distr_r :
   (A B C : U Prop),
    diff A (inter B C) = union (diff A B) (diff A C).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_union_l_diag :
   (A B : U Prop),
    diff (union A B) A = diff B A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_union_r_diag :
   (A B : U Prop),
    diff (union A B) B = diff A B.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_inter_l_diag :
   (A B : U Prop),
    diff A (inter A B) = diff A B.
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_inter_r_diag :
   (A B : U Prop),
    diff B (inter A B) = diff B A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_diff_l :
   (A B C : U Prop),
    union (diff A B) C = diff (union A C) (diff B C).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma union_diff_r :
   (A B C : U Prop),
    union A (diff B C) = diff (union A B) (diff C A).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma inter_diff_distr_l :
   (A B C : U Prop),
    inter A (diff B C) = diff (inter A B) (inter A C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_diff_distr_r :
   (A B C : U Prop),
    inter (diff A B) C = diff (inter A C) (inter B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff2_l :
   (A B C : U Prop),
    diff (diff A B) C = diff A (union B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff2_r :
   (A B C : U Prop),
    diff A (diff B C) = union (inter A C) (diff A B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff2_r_inter :
   (A B C : U Prop),
    incl A B
    diff A (diff B C) = inter A C.
Proof.
intros A B C H; apply diff_empty in H.
rewrite diff2_r H; apply union_empty_r.
Qed.

Lemma diff2 :
   (A B C D : U Prop),
    diff (diff A B) (diff C D) =
      union (diff (inter A (compl C)) B)
            (diff (inter A D) B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff2_diag_l :
   (A B C : U Prop),
    diff (diff A B) (diff A C) = diff (inter A C) B.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff2_cancel_left :
   (A B C : U Prop),
    incl A B
    diff (diff B C) (diff B A) = diff A C.
Proof.
intros; now rewrite diff2_diag_l inter_comm (proj1 (inter_left _ _)).
Qed.

Lemma diff2_diag_r :
   (A B C : U Prop),
    diff (diff A C) (diff B C) = diff (inter A (compl B)) C.
Proof.
intros; subset_ext_auto.
Qed.

End Diff_Facts.

Section Pair_Facts.

Context {U : Type}.

Lemma pair_correct : (a b x : U), pair a b x x = a x = b.
Proof. intros; split; (intros [Hx | Hx]; [left | right]); easy. Qed.

Lemma pair_sym : (a b : U), pair a b = pair b a.
Proof. intros; subset_ext_auto. Qed.

Lemma pair_in_l : (a b : U), pair a b a.
Proof. intros; apply incl_add_r; easy. Qed.

Lemma pair_in_r : (a b : U), pair a b b.
Proof. intros; apply add_in. Qed.

Lemma pair_in_l_alt : (a b x : U), x = a pair a b x.
Proof. intros; subst; apply pair_in_l. Qed.

Lemma pair_in_r_alt : (a b x : U), x = b pair a b x.
Proof. intros; subst; apply pair_in_r. Qed.

End Pair_Facts.

Section Sym_diff_Facts.

Facts about symmetric difference.

Context {U : Type}.
Lemma sym_diff_equiv_def_union :
   (A B : U Prop),
    sym_diff A B = union (diff A B) (diff B A).
Proof.
intros; subset_ext_auto.
Qed.

Lemma sym_diff_equiv_def_diff :
   (A B : U Prop),
    sym_diff A B = diff (union A B) (inter A B).
Proof.
intros; subset_ext_auto.
Qed.

Lemma union_equiv_def_sym_diff :
   (A B : U Prop),
    union A B = sym_diff (sym_diff A B) (inter A B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma inter_equiv_def_sym_diff :
   (A B : U Prop),
    inter A B = diff (union A B) (sym_diff A B).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma diff_equiv_def_sym_diff_inter :
   (A B : U Prop),
    diff A B = sym_diff A (inter A B).
Proof.
intros; subset_ext_auto.
Qed.

Lemma diff_equiv_def_sym_diff_union :
   (A B : U Prop),
    diff A B = sym_diff (union A B) B.
Proof.
intros; subset_ext_auto.
Qed.


Lemma sym_diff_assoc :
   (A B C : U Prop),
    sym_diff (sym_diff A B) C = sym_diff A (sym_diff B C).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma sym_diff_comm :
   (A B : U Prop),
    sym_diff A B = sym_diff B A.
Proof.
intros; subset_ext_auto.
Qed.

Lemma sym_diff_inv :
   (A : U Prop),
    sym_diff A A = emptyset.
Proof.
intros; subset_ext_auto.
Qed.

Lemma sym_diff_empty_l :
   (A : U Prop),
    sym_diff emptyset A = A.
Proof.
intros; rewrite sym_diff_equiv_def_union diff_empty_l diff_empty_r.
apply union_empty_l.
Qed.

Lemma sym_diff_empty_r :
   (A : U Prop),
    sym_diff A emptyset = A.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_empty_l.
Qed.

Lemma sym_diff_empty_l_rev :
   (A B : U Prop), sym_diff A B = B A = emptyset.
Proof.
unfold sym_diff; intros A B H.
rewrite -(inter_full_r A) -(union_compl_r B) inter_union_distr_l.
apply union_empty; split.
apply disj_equiv_def, disj_sym, diff_disj, subset_ext; split.
apply diff_lb_l.
intros Hx; split; [easy | assert (Hx1 : B x) by easy].
rewrite -H in Hx1; destruct Hx1 as [[_ Hx1] | [_ Hx1]]; easy.
apply empty_emptyset; intros x Hx.
generalize (union_ub_l _ (diff B A) _ Hx); rewrite H.
destruct Hx; easy.
Qed.

Lemma sym_diff_empty_r_rev :
   (A B : U Prop), sym_diff A B = A B = emptyset.
Proof. move=>>; rewrite sym_diff_comm; apply sym_diff_empty_l_rev. Qed.

Lemma sym_diff_eq_l :
   (A B : U Prop), sym_diff A B = A B = emptyset.
Proof.
intros; split;
    [apply sym_diff_empty_r_rev | intros; subst; apply sym_diff_empty_r].
Qed.

Lemma sym_diff_eq_r :
   (A B : U Prop), sym_diff A B = B A = emptyset.
Proof.
intros; split;
    [apply sym_diff_empty_l_rev | intros; subst; apply sym_diff_empty_l].
Qed.

Lemma sym_diff_full_l :
   (A : U Prop),
    sym_diff fullset A = compl A.
Proof.
intros; rewrite sym_diff_equiv_def_diff union_full_l inter_full_l.
symmetry; apply compl_equiv_def_diff.
Qed.

Lemma sym_diff_full_r :
   (A : U Prop),
    sym_diff A fullset = compl A.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_full_l.
Qed.

Lemma sym_diff_eq_reg_l :
   (A B C : U Prop),
    sym_diff A B = sym_diff A C B = C.
Proof.
intros A B C H.
rewrite -(sym_diff_empty_l B) -(sym_diff_empty_l C) -(sym_diff_inv A).
do 2 rewrite sym_diff_assoc.
now f_equal.
Qed.

Lemma sym_diff_eq_reg_r :
   (A B C : U Prop),
    sym_diff A B = sym_diff C B A = C.
Proof.
intros A B C H; apply sym_diff_eq_reg_l with B.
now rewrite (sym_diff_comm _ A) (sym_diff_comm _ C).
Qed.

Lemma sym_diff_compl_l :
   (A : U Prop),
    sym_diff (compl A) A = fullset.
Proof.
intros; rewrite -sym_diff_full_l sym_diff_assoc sym_diff_inv.
apply sym_diff_empty_r.
Qed.

Lemma sym_diff_compl_r :
   (A : U Prop),
    sym_diff A (compl A) = fullset.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_compl_l.
Qed.

Lemma sym_diff_compl :
   (A B : U Prop),
    sym_diff (compl A) (compl B) = sym_diff A B.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma union_sym_diff_super_distr_l :
   (A B C : U Prop),
    incl (sym_diff (union A C) (union B C))
         (union (sym_diff A B) C).
Proof.
intros; subset_auto.
Qed.

Lemma union_sym_diff_super_distr_r :
   (A B C : U Prop),
    incl (sym_diff (union A B) (union A C))
         (union A (sym_diff B C)).
Proof.
intros; subset_auto.
Qed.

Lemma union_sym_diff_super_distr :
   (A B C D : U Prop),
    incl (sym_diff (union A C) (union B D))
         (union (sym_diff A B) (sym_diff C D)).
Proof.
intros; subset_auto.
Qed.

Lemma sym_diff_union_sub_distr_l :
   (A B C : U Prop),
    incl (sym_diff (union A B) C)
         (union (sym_diff A C) (sym_diff B C)).
Proof.
intros; subset_auto.
Qed.

Lemma sym_diff_union_sub_distr_r :
   (A B C : U Prop),
    incl (sym_diff A (union B C))
         (union (sym_diff A B) (sym_diff A C)).
Proof.
intros; subset_auto.
Qed.

Lemma sym_diff_union_sub_distr :
   (A B C D : U Prop),
    incl (sym_diff (union A B) (union C D))
         (union (sym_diff A C) (sym_diff B D)).
Proof.
intros; subset_auto.
Qed.


Lemma inter_sym_diff_distr_l :
   (A B C : U Prop),
    inter (sym_diff A B) C = sym_diff (inter A C) (inter B C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_sym_diff_distr_r :
   (A B C : U Prop),
    inter A (sym_diff B C) = sym_diff (inter A B) (inter A C).
Proof.
intros; subset_ext_auto.
Qed.

Lemma inter_sym_diff_distr :
   (A B C D : U Prop),
    inter (sym_diff A B) (sym_diff C D) =
    sym_diff (sym_diff (inter A C) (inter A D))
             (sym_diff (inter B C) (inter B D)).
Proof.
intros; subset_ext_auto.
Qed.

Lemma sym_diff_inter_super_distr_l :
   (A B C : U Prop),
    incl (inter (sym_diff A C) (sym_diff B C))
         (sym_diff (inter A B) C).
Proof.
intros; subset_auto.
Qed.

Lemma sym_diff_inter_super_distr_r :
   (A B C : U Prop),
    incl (inter (sym_diff A B) (sym_diff A C))
         (sym_diff A (inter B C)).
Proof.
intros; subset_auto.
Qed.

Lemma sym_diff_inter_super_distr :
   (A B C D : U Prop),
    incl (inter (inter (sym_diff A C) (sym_diff A D))
                (inter (sym_diff B C) (sym_diff B D)))
         (sym_diff (inter A B) (inter C D)).
Proof.
intros; subset_auto.
Qed.


Lemma sym_diff_union :
   (A B : U Prop),
    sym_diff A B = union A B disj A B.
Proof.
intros; rewrite sym_diff_equiv_def_diff -diff_disj (disj_sym (union _ _)).
apply disj_inter_union.
Qed.

Lemma disj_sym_diff_inter :
   (A B : U Prop),
    disj (sym_diff A B) (inter A B).
Proof.
intros; subset_auto.
Qed.

Lemma union_sym_diff_inter :
   (A B : U Prop),
    union (sym_diff A B) (inter A B) = union A B.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma partition_union_sym_diff_inter :
   (A B : U Prop),
    partition (union A B) (sym_diff A B) (inter A B).
Proof.
intros; split.
symmetry; apply union_sym_diff_inter.
apply disj_sym_diff_inter.
Qed.

Lemma sym_diff_cancel_middle :
   (A B C : U Prop),
    sym_diff (sym_diff A B) (sym_diff B C) = sym_diff A C.
Proof.
intros; subset_ext_auto x.
Qed.

Lemma sym_diff2 :
   (A B C D : U Prop),
    sym_diff (sym_diff A B) (sym_diff C D) =
      sym_diff A (sym_diff B (sym_diff C D)).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma sym_diff_triangle_ineq :
   (A B C : U Prop),
    incl (sym_diff A C) (union (sym_diff A B) (sym_diff B C)).
Proof.
intros; intros x; subset_auto.
Qed.

Lemma sym_diff_diff_diag_l :
   (A B C : U Prop),
    incl (union B C) A
    sym_diff (diff A B) (diff A C) = sym_diff B C.
Proof.
intros A B C H; apply incl_union in H.
rewrite sym_diff_equiv_def_union.
repeat rewrite diff2_cancel_left; try easy.
now rewrite -sym_diff_equiv_def_union sym_diff_comm.
Qed.

End Sym_diff_Facts.

Section Partition_Facts.

Facts about partition.

Context {U : Type}.
Lemma partition_sym :
   (A B C : U Prop),
    partition A B C partition A C B.
Proof.
intros A B C; unfold partition.
now rewrite union_comm disj_sym.
Qed.

Lemma inter_partition_compat_l :
   (A B C D : U Prop),
    partition A B C partition (inter D A) (inter D B) (inter D C).
Proof.
intros A B C D [H1 H2]; split.
rewrite H1; apply inter_union_distr_l.
now apply inter_disj_compat_l.
Qed.

Lemma inter_partition_compat_r :
   (A B C D : U Prop),
    partition A B C partition (inter A D) (inter B D) (inter C D).
Proof.
intros A B C D.
rewrite (inter_comm A) (inter_comm B) (inter_comm C).
apply inter_partition_compat_l.
Qed.

Lemma diff_partition_compat_r :
   (A B C D : U Prop),
    partition A B C partition (diff A D) (diff B D) (diff C D).
Proof.
intros; now apply inter_partition_compat_r.
Qed.

End Partition_Facts.

Section Prod_Facts.

Facts about Cartesian product.

Context {U1 U2 : Type}.
Lemma inhabited_prod :
  inhabited U1 inhabited U2 inhabited (U1 × U2).
Proof.
intros [x1] [x2]; apply (inhabits (x1, x2)).
Qed.

Lemma prod_empty_l :
   A2, prod emptyset A2 = @emptyset (U1 × U2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_empty_r :
   A1, prod A1 emptyset = @emptyset (U1 × U2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full :
  prod fullset fullset = @fullset (U1 × U2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full_l :
   A2, prod fullset A2 = fun x : U1 × U2A2 (snd x).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full_r :
   A1, prod A1 fullset = fun x : U1 × U2A1 (fst x).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_equiv :
   (A1 : U1 Prop) (A2 : U2 Prop),
    prod A1 A2 = inter (prod A1 fullset) (prod fullset A2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_compl_full :
   A1 : U1 Prop,
    prod (compl A1) (@fullset U2) = compl (prod A1 fullset).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full_compl :
   A2 : U2 Prop,
    prod (@fullset U1) (compl A2) = compl (prod fullset A2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_union_full :
   A1 B1 : U1 Prop,
    prod (union A1 B1) (@fullset U2) = union (prod A1 fullset) (prod B1 fullset).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full_union :
   A2 B2 : U2 Prop,
    prod (@fullset U1) (union A2 B2) = union (prod fullset A2) (prod fullset B2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_inter_full :
   A1 B1 : U1 Prop,
    prod (inter A1 B1) (@fullset U2) = inter (prod A1 fullset) (prod B1 fullset).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_full_inter :
   A2 B2 : U2 Prop,
    prod (@fullset U1) (inter A2 B2) = inter (prod fullset A2) (prod fullset B2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_inter :
   (A1 B1 : U1 Prop) (A2 B2 : U2 Prop),
    inter (prod A1 A2) (prod B1 B2) = prod (inter A1 B1) (inter A2 B2).
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_compl_union :
   (A1 : U1 Prop) (A2 : U2 Prop),
    compl (prod A1 A2) = union (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
intros; subset_ext_auto x.
Qed.

Lemma prod_compl_disj :
   (A1 : U1 Prop) (A2 : U2 Prop),
    disj (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
subset_auto.
Qed.

Lemma prod_compl_partition :
   (A1 : U1 Prop) (A2 : U2 Prop),
    partition (compl (prod A1 A2))
      (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
intros; split.
apply prod_compl_union.
apply prod_compl_disj.
Qed.

Lemma swap_c_prod:
   (A1 : U1 Prop) (A2 : U2 Prop), swap_c (prod A1 A2) = prod A2 A1.
Proof.
intros; subset_ext_auto.
Qed.

Lemma prod_swap_c :
   (A1 : U1 Prop) (A2 : U2 Prop),
    (fun x21 : U2 × U1prod A1 A2 (swap_c (fun x : U1 × U2x) x21)) =
      prod A2 A1.
Proof.
intros; subset_ext_auto.
Qed.

Lemma swap_c_invol : A : U1 × U2 Prop, swap_c (swap_c A) = A.
Proof.
intros; subset_ext_auto.
Qed.

End Prod_Facts.