(* This program 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 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program 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      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Fpart.
Require Export Inter.
Require Export Arith.
Section fparts2_def.
Variable E : Setoid.

Definition disjoint (A B : part_set E) := Equal (inter A B) (empty E).

Lemma disjoint_comp :
 forall A A' B B' : part_set E,
 Equal A A' -> Equal B B' -> disjoint A B -> disjoint A' B'.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : disjoint A B) (_ : @in_part E x A), not (@in_part E x B) *)
unfold disjoint in |- *.
(* Goal: forall (A A' B B' : Carrier (part_set E)) (_ : @Equal (part_set E) A A') (_ : @Equal (part_set E) B B') (_ : @Equal (part_set E) (@inter E A B) (empty E)), @Equal (part_set E) (@inter E A' B') (empty E) *)
intros A A' B B' H' H'0 H'1; try assumption.
(* Goal: @Equal (part_set E) (@inter E A' B') (empty E) *)
apply Trans with (inter A B).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.

Lemma empty_not_in :
 forall A : part_set E, Equal A (empty E) -> forall x : E, ~ in_part x A.
(* Goal: forall (A : Carrier (part_set E)) (_ : @Equal (part_set E) A (empty E)) (x : Carrier E), not (@in_part E x A) *)
intros A; case A; intros a pa; simpl in |- *.
(* Goal: forall (_ : @eq_part E (@Build_Predicate E a pa) (empty E)) (x : Carrier E), not (a x) *)
unfold eq_part, empty in |- *; simpl in |- *.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
intros.
(* Goal: @cardinal E B0 n *)
elim (H x); auto with *.
Qed.

Lemma disjoint_inclus :
 forall A B C : part_set E, included A B -> disjoint B C -> disjoint A C.
(* Goal: forall (A B C : Carrier (part_set E)) (_ : @included E A B) (_ : disjoint B C), disjoint A C *)
unfold included, disjoint in |- *.
(* Goal: forall (A B C : Carrier (part_set E)) (_ : forall (x : Carrier E) (_ : @in_part E x A), @in_part E x B) (_ : @Equal (part_set E) (@inter E B C) (empty E)), @Equal (part_set E) (@inter E A C) (empty E) *)
intros A B C H' H'0; try assumption.
(* Goal: @Equal (part_set E) (@inter E A (@diff E B A)) (empty E) *)
apply not_in_empty.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
cut (in_part x (inter B C)).
(* Goal: forall _ : @in_part E x (@inter E B C), False *)
(* Goal: @in_part E x (@inter E B C) *)
generalize (empty_not_in (A:=inter B C) H'0).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
(* Goal: @in_part E x (@inter E B C) *)
apply H0 with (x := x).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @in_part E x (@inter E B C) *)
apply in_part_inter.
(* Goal: @in_part E x B *)
(* Goal: @in_part E x C *)
apply H'.
(* Goal: @in_part E x A *)
(* Goal: @in_part E x C *)
apply in_part_inter_l with C.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @in_part E x C *)
apply in_part_inter_r with A.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.

Lemma included_add_part :
 forall (A : part_set E) (x : E), included A (add_part A x).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E), @included E A (@add_part E A x) *)
intros A x; red in |- *.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.
Hint Resolve included_add_part: algebra.

Lemma union_not_in :
 forall (A B : part_set E) (x : E),
 ~ in_part x A -> ~ in_part x B -> ~ in_part x (union A B).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
cut (in_part x A \/ in_part x B).
(* Goal: forall _ : @in_part E x (@diff E (empty E) A), @in_part E x (empty E) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@diff E (empty E) A) *)
intros H'; try assumption.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.
Hint Resolve union_not_in: algebra.

Lemma disjoint_not_in_r :
 forall (A B : part_set E) (x : E),
 disjoint A B -> in_part x A -> ~ in_part x B.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : disjoint A B) (_ : @in_part E x A), not (@in_part E x B) *)
unfold disjoint in |- *.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
cut (in_part x (empty E)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @in_part E x (empty E) *)
apply in_part_comp_r with (inter A B).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.

Lemma cardinal_union_disjoint :
 forall (a b : nat) (A B : part_set E),
 cardinal A a -> cardinal B b -> disjoint A B -> cardinal (union A B) (a + b).
(* Goal: forall (a b : nat) (A B : Carrier (part_set E)) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : disjoint A B), @cardinal E (@union E A B) (Init.Nat.add a b) *)
simple induction a.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
intros.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with (union (empty E) B); auto with *.
(* Goal: @cardinal E B0 n *)
apply union_comp; auto with *.
(* Goal: @Equal (part_set E) (empty E) (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply Sym.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with B; auto with *.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
intros.
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
inversion H0.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
simpl in |- *.
(* Goal: @cardinal E B0 n *)
apply cardinal_add with (union B0 B) x; auto with *.
(* Goal: @cardinal E B0 n *)
apply H; auto with *.
(* Goal: @cardinal E B0 n *)
apply disjoint_inclus with (add_part B0 x); auto with *.
(* Goal: @cardinal E B0 n *)
apply disjoint_comp with A B; auto with *.
(* Goal: @cardinal E B0 n *)
apply union_not_in; auto with *.
(* Goal: @cardinal E B0 n *)
apply disjoint_not_in_r with A; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_comp_r with (add_part B0 x); auto with *.
(* Goal: @cardinal E B0 n *)
apply Trans with (union (add_part B0 x) B); auto with *.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: @cardinal E B0 n *)
apply Trans with (union B0 (union (single x) B)); auto with *.
(* Goal: @cardinal E B0 n *)
apply Trans with (union B0 (union B (single x))); auto with *.
Qed.
Hint Resolve cardinal_union_disjoint: algebra.

Lemma in_eq_part :
 forall A B : part_set E,
 (forall x : E, in_part x A -> in_part x B) ->
 (forall x : E, in_part x B -> in_part x A) -> Equal A B.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A) (_ : not (@in_part E x B)), @in_part E x (@diff E A B) *)
intros A B.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun0) (x : Carrier E) (_ : Pred_fun0 x) (_ : not (Pred_fun x)), and (Pred_fun0 x) (not (Pred_fun x)) *)
intros a pa b pb.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
Qed.

Lemma diff_in_l :
 forall (A B : part_set E) (x : E), in_part x (diff A B) -> in_part x A.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A) (_ : not (@in_part E x B)), @in_part E x (@diff E A B) *)
intros A B.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun0) (x : Carrier E) (_ : Pred_fun0 x) (_ : not (Pred_fun x)), and (Pred_fun0 x) (not (Pred_fun x)) *)
intros a pa b pb.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
Qed.

Lemma diff_in_r :
 forall (A B : part_set E) (x : E), in_part x (diff A B) -> ~ in_part x B.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A) (_ : not (@in_part E x B)), @in_part E x (@diff E A B) *)
intros A B.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun0) (x : Carrier E) (_ : Pred_fun0 x) (_ : not (Pred_fun x)), and (Pred_fun0 x) (not (Pred_fun x)) *)
intros a pa b pb.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
Qed.

Lemma in_diff :
 forall (A B : part_set E) (x : E),
 in_part x A -> ~ in_part x B -> in_part x (diff A B).
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A) (_ : not (@in_part E x B)), @in_part E x (@diff E A B) *)
intros A B.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun0) (x : Carrier E) (_ : Pred_fun0 x) (_ : not (Pred_fun x)), and (Pred_fun0 x) (not (Pred_fun x)) *)
intros a pa b pb.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: forall (x : Carrier E) (_ : b x) (_ : not (a x)), and (b x) (not (a x)) *)
intuition.
Qed.
Hint Resolve in_diff: algebra.

Lemma union_diff :
 forall A B : part_set E, Equal (union A (diff B A)) (union A B).
(* Goal: forall A B : Carrier (part_set E), @Equal (part_set E) (@inter E A (@diff E B A)) (empty E) *)
intros A B; try assumption.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@inter E (empty E) A) *)
intros x H'; try assumption.
(* Goal: @in_part E x (@union E A (@diff E B A)) *)
elim (in_part_union H').
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: forall _ : @in_part E x B, @in_part E x (@union E A (@diff E B A)) *)
intros H'0; try assumption.
(* Goal: @in_part E x (@union E A B) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@union E A B)), @in_part E x (@union E A (@diff E B A)) *)
cut (in_part x B).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @in_part E x B *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@union E A B)), @in_part E x (@union E A (@diff E B A)) *)
exact (diff_in_l H'0).
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@inter E (empty E) A) *)
intros x H'; try assumption.
(* Goal: @in_part E x (@union E A (@diff E B A)) *)
elim (in_part_union H').
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: forall _ : @in_part E x B, @in_part E x (@union E A (@diff E B A)) *)
intros H'0; try assumption.
(* Goal: @in_part E x (@union E A (@diff E B A)) *)
elim (classic (in_part x A)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: forall _ : not (@in_part E x A), @in_part E x (@union E A (@diff E B A)) *)
intros H'1; try assumption.
(* Goal: @in_part E x (@union E A (@diff E B A)) *)
cut (in_part x (diff B A)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.
Hint Resolve union_diff: algebra.

Lemma disjoint_diff : forall A B : part_set E, disjoint A (diff B A).
(* Goal: forall A B : Carrier (part_set E), disjoint A (@diff E B A) *)
red in |- *.
(* Goal: forall A B : Carrier (part_set E), @Equal (part_set E) (@inter E A (@diff E B A)) (empty E) *)
intros A B; try assumption.
(* Goal: @Equal (part_set E) (@inter E A (@diff E B A)) (empty E) *)
apply not_in_empty.
(* Goal: forall x : Carrier E, not (@in_part E x (@inter E A (@diff E B A))) *)
intros x; red in |- *; intros H'; try exact H'.
(* Goal: False *)
absurd (in_part x A).
(* Goal: not (@in_part E x A) *)
(* Goal: @in_part E x A *)
apply diff_in_r with B.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_inter_r with A; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_inter_l with (diff B A); auto with *.
Qed.
Hint Resolve disjoint_diff: algebra.

Lemma cardinal_union :
 forall (a b : nat) (A B : part_set E),
 cardinal A a -> cardinal (diff B A) b -> cardinal (union A B) (a + b).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
intros.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with (union A (diff B A)); auto with *.
Qed.
Hint Resolve cardinal_union: algebra.

Lemma empty_diff : forall A : part_set E, Equal (diff (empty E) A) (empty E).
(* Goal: forall A : Carrier (part_set E), @Equal (part_set E) (@inter E (empty E) A) (empty E) *)
intros A; try assumption.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@diff E (empty E) A)), @in_part E x (empty E) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@diff E (empty E) A) *)
intro.
(* Goal: forall _ : @in_part E x (@diff E (empty E) A), @in_part E x (empty E) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@diff E (empty E) A) *)
intros H'; try assumption.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with A; auto with *.
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@inter E (empty E) A) *)
intros x H'; try assumption.
(* Goal: @cardinal E B0 n *)
absurd (in_part x (empty E)); auto with *.
Qed.
Hint Resolve empty_diff: algebra.

Lemma empty_inter :
 forall A : part_set E, Equal (inter (empty E) A) (empty E).
(* Goal: forall A : Carrier (part_set E), @Equal (part_set E) (@inter E (empty E) A) (empty E) *)
intros A; try assumption.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@inter E (empty E) A) *)
intros x H'; try assumption.
(* Goal: @cardinal E B0 n *)
apply in_part_inter_l with A; auto with *.
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@inter E (empty E) A) *)
intros x H'; try assumption.
(* Goal: @cardinal E B0 n *)
absurd (in_part x (empty E)); auto with *.
Qed.
Hint Resolve empty_inter: algebra.

Lemma in_part_trans_eq :
 forall (A : part_set E) (x y : E), in_part x A -> Equal y x -> in_part y A.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
intros A; case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : @pred_compatible E Pred_fun) (x y : Carrier E) (_ : Pred_fun x) (_ : @Equal E y x), Pred_fun y *)
intros a pa.
(* Goal: forall (x y : Carrier E) (_ : a x) (_ : @Equal E y x), a y *)
intros x y H' H'0; try assumption.
(* Goal: @cardinal E B0 n *)
apply pa with x; auto with *.
Qed.

Lemma diff_add_part :
 forall (A B0 B : part_set E) (x : E),
 ~ in_part x B0 ->
 Equal A (add_part B0 x) -> in_part x B -> Equal (diff B0 B) (diff A B).
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@union E B0 (@single E x))) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
intros A B0 B x H' H'0 H'1; try assumption.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @in_part E x0 (@diff E A B) *)
apply in_diff.
(* Goal: @in_part E x0 A *)
(* Goal: not (@in_part E x0 B) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@diff E A B)), @in_part E x (@diff E B0 B) *)
apply in_part_comp_r with (add_part B0 x).
(* Goal: @in_part E x0 (@add_part E B0 x) *)
(* Goal: @Equal (part_set E) (@add_part E B0 x) A *)
(* Goal: not (@in_part E x0 B) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@diff E A B)), @in_part E x (@diff E B0 B) *)
cut (in_part x0 B0).
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with B; auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_r with B0; auto with *.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: not (@in_part E x0 B) *)
elim (classic (Equal x0 x)).
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @cardinal E B0 n *)
absurd (in_part x B); auto with *.
(* Goal: not (@in_part E x B) *)
(* Goal: forall _ : not (@Equal E x0 x), @in_part E x0 (@diff E B0 B) *)
cut (in_part x (diff A B)).
(* Goal: forall _ : @in_part E x0 (@single E x), @in_part E x0 B0 *)
(* Goal: not (@in_part E x0 B) *)
intros H'4; try assumption.
(* Goal: @cardinal E B0 n *)
apply diff_in_r with A; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x0; auto with *.
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @in_part E x0 (@diff E A B) *)
apply in_diff.
(* Goal: @cardinal E B0 n *)
apply add_part_in_el_diff with x; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_comp_r with A; auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with B; auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_r with A; auto with *.
Qed.

Lemma diff_not_in :
 forall (A B : part_set E) (x : E), ~ in_part x A -> ~ in_part x (diff A B).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
apply H.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with B; auto with *.
Qed.
Hint Resolve diff_not_in: algebra.

Lemma inter_not_in :
 forall (A B : part_set E) (x : E), ~ in_part x A -> ~ in_part x (inter A B).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
apply H.
(* Goal: @cardinal E B0 n *)
apply in_part_inter_l with B; auto with *.
Qed.
Hint Resolve inter_not_in: algebra.
(* OK *)

Lemma inter_add_part :
 forall (A B0 B : part_set E) (x : E),
 ~ in_part x B0 ->
 Equal A (add_part B0 x) ->
 in_part x B -> Equal (inter A B) (add_part (inter B0 B) x).
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@union E B0 (@single E x))) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
intros A B0 B x H' H'0 H'1; try assumption.
(* Goal: @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
apply Trans with (inter (union B0 (single x)) B).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @Equal (part_set E) (@inter E B0 B) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply Trans with (union (inter B0 B) (inter (single x) B)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply union_comp; auto with *.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @cardinal E B0 n *)
apply in_part_inter_l with B; auto with *.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @cardinal E B0 n *)
apply in_part_inter; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x; auto with *.
Qed.
Hint Resolve inter_add_part: algebra.

Lemma diff_add_part_not_in :
 forall (A B0 B : part_set E) (x : E),
 ~ in_part x B0 ->
 Equal A (add_part B0 x) ->
 ~ in_part x B -> Equal (diff A B) (add_part (diff B0 B) x).
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@union E B0 (@single E x))) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
intros A B0 B x H' H'0 H'1; try assumption.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: not (@in_part E x0 B) *)
elim (classic (Equal x0 x)).
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x; auto with *.
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: @in_part E x0 (@union E B0 (@single E x)) *)
(* Goal: not (@in_part E x0 B) *)
apply in_part_union_or.
(* Goal: or (@in_part E x0 B0) (@in_part E x0 (@single E x)) *)
(* Goal: not (@in_part E x0 B) *)
left.
(* Goal: @in_part E x0 (@diff E A B) *)
apply in_diff.
(* Goal: @cardinal E B0 n *)
apply add_part_in_el_diff with x; auto with *.
(* Goal: @cardinal E B0 n *)
apply in_part_comp_r with A; auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with B; auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_in_r with A; auto with *.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @in_part E x0 (@diff E A B) *)
apply in_diff.
(* Goal: @cardinal E B0 n *)
apply in_part_comp_r with (add_part B0 x); auto with *.
(* Goal: not (@in_part E x0 B) *)
elim (classic (Equal x0 x)).
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x; auto with *.
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: @in_part E x0 (@union E B0 (@single E x)) *)
(* Goal: not (@in_part E x0 B) *)
apply in_part_union_or.
(* Goal: or (@in_part E x0 B0) (@in_part E x0 (@single E x)) *)
(* Goal: not (@in_part E x0 B) *)
left.
(* Goal: @in_part E x0 B0 *)
(* Goal: not (@in_part E x0 B) *)
unfold add_part in H'2.
(* Goal: @in_part E x0 B0 *)
(* Goal: not (@in_part E x0 B) *)
elim (in_part_union H'2).
(* Goal: forall _ : @in_part E x0 (@single E x), @in_part E x0 B0 *)
(* Goal: not (@in_part E x0 B) *)
intros H'4; try assumption.
(* Goal: @cardinal E B0 n *)
apply diff_in_l with B; auto with *.
(* Goal: forall _ : @in_part E x0 (@single E x), @in_part E x0 B0 *)
(* Goal: not (@in_part E x0 B) *)
intros H'4; try assumption.
(* Goal: @cardinal E B0 n *)
absurd (in_part x0 (single x)); auto with *.
(* Goal: not (@in_part E x0 B) *)
elim (classic (Equal x0 x)).
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
unfold not in |- *; intros.
(* Goal: False *)
(* Goal: @in_part E x0 B *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
unfold not in H'1.
(* Goal: False *)
(* Goal: @in_part E x0 B *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply H'1.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x0; auto with *.
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @cardinal E B0 n *)
apply diff_in_r with B0; auto with *.
(* Goal: @cardinal E B0 n *)
apply add_part_in_el_diff with x; auto with *.
Qed.
Hint Resolve diff_add_part_not_in: algebra.

Lemma inter_add_part_not_in :
 forall (A B0 B : part_set E) (x : E),
 ~ in_part x B0 ->
 Equal A (add_part B0 x) -> ~ in_part x B -> Equal (inter B0 B) (inter A B).
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@add_part E B0 x)) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
unfold add_part in |- *.
(* Goal: forall (A B0 B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B0)) (_ : @Equal (part_set E) A (@union E B0 (@single E x))) (_ : not (@in_part E x B)), @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
intros A B0 B x H' H'0 H'1; try assumption.
(* Goal: @Equal (part_set E) (@inter E B0 B) (@inter E A B) *)
apply Trans with (inter (union B0 (single x)) B).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @Equal (part_set E) (@inter E B0 B) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply Trans with (union (inter B0 B) (inter (single x) B)).
(* Goal: @Equal (part_set E) (@inter E B0 B) (@union E (@inter E B0 B) (@inter E (@single E x) B)) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply Trans with (union (inter B0 B) (empty E)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
apply union_comp; auto with *.
(* Goal: @Equal (part_set E) (empty E) (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply Sym.
(* Goal: @Equal (part_set E) (@inter E (@single E x) B) (empty E) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_eq_part.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @in_part E x0 (empty E) *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
cut (Equal x x0).
(* Goal: forall _ : @Equal E x x0, @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros H'3; try assumption.
(* Goal: @in_part E x0 (empty E) *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
absurd (in_part x0 B).
(* Goal: forall (x : Carrier E) (_ : @in_part E x (@diff E (empty E) A)), @in_part E x (empty E) *)
(* Goal: forall (x : Carrier E) (_ : @in_part E x (empty E)), @in_part E x (@diff E (empty E) A) *)
unfold not in |- *; intro.
(* Goal: False *)
(* Goal: @in_part E x0 B *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
unfold not in H'1.
(* Goal: False *)
(* Goal: @in_part E x0 B *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply H'1.
(* Goal: @cardinal E B0 n *)
apply in_part_trans_eq with x0; auto with *.
(* Goal: @in_part E x0 B *)
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_part_inter_r with (single x).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @Equal E x x0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
cut (in_part x0 (single x)).
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @in_part E x0 (@single E x) *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
apply in_part_inter_l with B.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (empty E)), @in_part E x0 (@inter E (@single E x) B) *)
(* Goal: @Equal (part_set E) (@union E (@inter E B0 B) (@inter E (@single E x) B)) (@inter E (@union E B0 (@single E x)) B) *)
(* Goal: @Equal (part_set E) (@inter E (@union E B0 (@single E x)) B) (@inter E A B) *)
intros x0 H'2; try assumption.
(* Goal: @cardinal E B0 n *)
absurd (in_part x0 (empty E)); auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.

Lemma cardinal_diff :
 forall (a : nat) (A B : part_set E),
 cardinal A a ->
 exists b : nat,
   (exists c : nat,
      cardinal (diff A B) b /\ cardinal (inter A B) c /\ a = b + c).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
simple induction a; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
exists 0; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
exists 0; intros.
(* Goal: and (@cardinal E (@diff E A B) O) (and (@cardinal E (@inter E A B) O) (@eq nat O (Init.Nat.add O O))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
simpl in |- *.
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E (@inter E A B) O *)
(* Goal: @eq nat O O *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
apply cardinal_empty.
(* Goal: @cardinal E B0 n *)
apply Trans with (diff (empty E) B); auto with *.
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E (@inter E A B) O *)
(* Goal: @eq nat O O *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
apply cardinal_empty.
(* Goal: @cardinal E B0 n *)
apply Trans with (inter (empty E) B); auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
inversion H0.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
elim (H B0 B); intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H6; clear H6; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H6; clear H6; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H7; clear H7; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case (classic (in_part x B)); intros.
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
(* Goal: @cardinal E B0 n *)
exists x0.
(* Goal: @ex nat (fun c : nat => and (@cardinal E (@diff E A B) x0) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add x0 c)))) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
(* Goal: @cardinal E B0 n *)
exists (S x1).
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with (diff B0 B); auto with *.
(* Goal: @cardinal E B0 n *)
apply diff_add_part with x; auto with *.
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E B0 n *)
apply cardinal_add with (inter B0 B) x; auto with *.
(* Goal: @eq nat (S n) (Init.Nat.add x0 (S x1)) *)
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
(* Goal: @cardinal E B0 n *)
rewrite H8.
(* Goal: @cardinal E B0 n *)
auto with *.
(* Goal: @ex nat (fun b : nat => @ex nat (fun c : nat => and (@cardinal E (@diff E A B) b) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add b c))))) *)
(* Goal: @cardinal E B0 n *)
exists (S x0).
(* Goal: @ex nat (fun c : nat => and (@cardinal E (@diff E A B) (S x0)) (and (@cardinal E (@inter E A B) c) (@eq nat (S n) (Init.Nat.add (S x0) c)))) *)
(* Goal: @cardinal E B0 n *)
exists x1.
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E B0 n *)
apply cardinal_add with (diff B0 B) x; auto with *.
(* Goal: and (@cardinal E (@inter E A B) x1) (@eq nat (S n) (Init.Nat.add (S x0) x1)) *)
(* Goal: @cardinal E B0 n *)
split.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with (inter B0 B); auto with *.
(* Goal: @cardinal E B0 n *)
apply inter_add_part_not_in with x; auto with *.
(* Goal: @cardinal E B0 n *)
rewrite H8; auto with *.
(* Goal: @cardinal E B0 n *)
auto with *.
Qed.

Lemma cardinal_union_inter :
 forall (A B : part_set E) (a b c : nat),
 cardinal A a ->
 cardinal B b -> cardinal (inter A B) c -> cardinal (union A B) (a + b - c).
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case (cardinal_diff A H0); intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H2; clear H2; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H2; clear H2; intros.
(* Goal: forall (A B : Carrier (part_set E)) (a b c : nat) (_ : @cardinal E A a) (_ : @cardinal E B b) (_ : @cardinal E (@inter E A B) c), @cardinal E (@union E A B) (Init.Nat.sub (Init.Nat.add a b) c) *)
case H3; clear H3; intros.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp with (union A (diff B A)) (a + x); auto with *.
(* Goal: @eq nat (Init.Nat.add a x) (Init.Nat.sub (Init.Nat.add a b) c) *)
rewrite H4.
(* Goal: @eq nat (Init.Nat.add a x) (Init.Nat.sub (Init.Nat.add a (Init.Nat.add x x0)) c) *)
replace c with x0.
(* Goal: @eq nat (Init.Nat.add a x) (Init.Nat.sub (Init.Nat.add a (Init.Nat.add x x0)) x0) *)
(* Goal: @eq nat x0 c *)
rewrite plus_assoc.
(* Goal: @cardinal E B0 n *)
replace (a + x + x0) with (x0 + (a + x)); auto with *.
(* Goal: @cardinal E B0 n *)
apply (cardinal_unique H3); auto with *.
(* Goal: @cardinal E B0 n *)
apply cardinal_comp_l with (inter A B); auto with *.
Qed.
Hint Resolve cardinal_union_inter: algebra.
End fparts2_def.
