(* 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 Union.
Require Export Singleton.
Require Export Diff.
Require Export Classical_Prop.
Section fparts_in_def.
Variable E : Setoid.

(*
	Add_part.
*)

Definition add_part (A : part_set E) (x : E) := union A (single x).

Lemma add_part_comp :
 forall (A A' : part_set E) (x x' : E),
 Equal A A' -> Equal x x' -> Equal (add_part A x) (add_part A' x').
(* Goal: forall (A A' : Carrier (part_set E)) (x x' : Carrier E) (_ : @Equal (part_set E) A A') (_ : @Equal E x x'), @Equal (part_set E) (add_part A x) (add_part A' x') *)
unfold add_part in |- *; auto with algebra.
Qed.
Hint Resolve add_part_comp: algebra.

Lemma add_part_in : forall (A : part_set E) (x : E), in_part x (add_part A x).
(* Goal: forall (A : Carrier (part_set E)) (x : Carrier E), @in_part E x (add_part A x) *)
simpl in |- *; auto with algebra.
Qed.
Hint Resolve add_part_in: algebra.

Lemma add_part_com :
 forall (A : part_set E) (x y : E),
 Equal (add_part (add_part A x) y) (add_part (add_part A y) x).
(* Goal: forall x : Carrier E, @Equal (part_set E) (@single E x) (add_part (empty E) x) *)
unfold add_part in |- *.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @Equal (part_set E) (@union E (@union E A (@single E x)) (@single E y)) (@union E (@union E A (@single E y)) (@single E x)) *)
apply Trans with (union A (union (single x) (single y))); auto with algebra.
(* Goal: @Equal (part_set E) (@union E A (@union E (@single E x) (@single E y))) (@union E (@union E A (@single E y)) (@single E x)) *)
apply Trans with (union A (union (single y) (single x))); auto with algebra.
Qed.
Hint Immediate add_part_com: algebra.

Lemma add_in :
 forall (A : part_set E) (x : E), in_part x A -> Equal (add_part A x) A.
(* Goal: forall (A : Predicate E) (x : Carrier E) (_ : not (@in_part E x A)) (x0 : Carrier E), and (forall _ : and (@in_part E x0 A) (not (@Equal E x0 x)), @in_part E x0 A) (forall _ : @in_part E x0 A, and (@in_part E x0 A) (not (@Equal E x0 x))) *)
intro A.
(* Goal: forall _ : forall x : Carrier E, not (@in_part E x A), @Equal (part_set E) A (empty E) *)
case A.
simpl in |- *; unfold pred_compatible, eq_part, in_part in |- *;
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
 simpl in |- *.
(* Goal: forall (_ : forall x : Carrier E, not (a x)) (x : Carrier E), and (forall _ : a x, False) (forall _ : False, a x) *)
intuition eauto.
Qed.
Hint Resolve add_in: algebra.

Lemma add_part_in_el_diff :
 forall (A : part_set E) (x y : E),
 in_part y (add_part A x) -> ~ Equal y x -> in_part y A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, add_part, union, single in |- *; simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.

Lemma add_part_in_el_not_in :
 forall (A : part_set E) (x y : E),
 in_part y (add_part A x) -> ~ in_part y A -> Equal y x.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, add_part, union, single in |- *; simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.

Lemma add_part_simpl :
 forall (A B : part_set E) (x : E),
 ~ in_part x A ->
 ~ in_part x B -> Equal (add_part A x) (add_part B x) -> Equal A B.
(* Goal: forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x A)) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) (add_part A x) (add_part B x)), @Equal (part_set E) A B *)
intros A B.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (Pred_compatible_prf0 : @pred_compatible E Pred_fun0) (_ : not (Pred_fun0 x)) (_ : @eq_part E (@Build_Predicate E Pred_fun0 Pred_compatible_prf0) (@Build_Predicate E Pred_fun Pred_compatible_prf)), not (Pred_fun x) *)
intros a pa b pb.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, add_part, union, single in |- *; simpl in |- *.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (classic (Equal x x0)); intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
split; intros.
(* Goal: a x0 *)
(* Goal: or (and (a x0) (forall _ : @Equal E x0 x, False)) (@Equal E x0 x) *)
apply pa with x; auto with algebra.
(* Goal: a x *)
(* Goal: b x0 *)
(* Goal: and (forall _ : b x0, a x0) (forall _ : a x0, b x0) *)
cut (b x).
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: a x *)
(* Goal: b x *)
(* Goal: b x0 *)
(* Goal: and (forall _ : b x0, a x0) (forall _ : a x0, b x0) *)
absurd (b x); auto with algebra.
(* Goal: b x *)
(* Goal: b x0 *)
(* Goal: and (forall _ : b x0, a x0) (forall _ : a x0, b x0) *)
apply pb with x0; auto with algebra.
(* Goal: b x0 *)
(* Goal: and (forall _ : b x0, a x0) (forall _ : a x0, b x0) *)
cut (a x).
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: b x0 *)
(* Goal: a x *)
(* Goal: and (forall _ : b x0, a x0) (forall _ : a x0, b x0) *)
absurd (a x); auto with algebra.
(* Goal: a x *)
apply pa with x0; auto with algebra.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (H1 x0); intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
split; intros.
(* Goal: a x0 *)
(* Goal: b x0 *)
lapply H3.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim H6; intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
absurd (Equal x0 x); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
left; auto with algebra.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
lapply H4; intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim H6; intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
absurd (Equal x0 x); auto with algebra.
(* Goal: or (a x0) (@Equal E x0 x) *)
left.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
Qed.

(*
	Minus_part.
*)

Definition minus_part (A : part_set E) (x : E) := diff A (single x).

Lemma minus_part_comp :
 forall (A A' : part_set E) (x x' : E),
 Equal A A' -> Equal x x' -> Equal (minus_part A x) (minus_part A' x').
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
unfold minus_part in |- *; auto with algebra.
Qed.
Hint Resolve minus_part_comp: algebra.

Lemma minus_part_not_in :
 forall (A : part_set E) (x : E), ~ in_part x (minus_part A x).
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.
Hint Resolve minus_part_not_in: algebra.

Lemma minus_part_com :
 forall (A : part_set E) (x y : E),
 Equal (minus_part (minus_part A x) y) (minus_part (minus_part A y) x).
(* Goal: forall (A : Carrier (part_set E)) (x y : Carrier E), @Equal (part_set E) (minus_part (minus_part A x) y) (minus_part (minus_part A y) x) *)
unfold minus_part in |- *.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, diff, single in |- *; simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.
Hint Immediate minus_part_com: algebra.

Lemma minus_not_in :
 forall (A : part_set E) (x : E), ~ in_part x A -> Equal (minus_part A x) A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, minus_part, diff, single in |- *; simpl in |- *.
(* Goal: forall (A : Predicate E) (x : Carrier E) (_ : not (@in_part E x A)) (x0 : Carrier E), and (forall _ : and (@in_part E x0 A) (not (@Equal E x0 x)), @in_part E x0 A) (forall _ : @in_part E x0 A, and (@in_part E x0 A) (not (@Equal E x0 x))) *)
intro A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; unfold pred_compatible in |- *; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (_ : forall (x y : Carrier E) (_ : Pred_fun x) (_ : @Equal E y x), Pred_fun y) (x : Carrier E) (_ : not (Pred_fun x)) (x0 : Carrier E), and (forall _ : and (Pred_fun x0) (not (@Equal E x0 x)), Pred_fun x0) (forall _ : Pred_fun x0, and (Pred_fun x0) (not (@Equal E x0 x))) *)
intros a pa x neg_a_x x0.
(* Goal: and (forall _ : and (a x0) (not (@Equal E x0 x)), a x0) (forall _ : a x0, and (a x0) (not (@Equal E x0 x))) *)
generalize (pa x0 x).
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intuition auto with algebra.
Qed.
Hint Resolve minus_not_in: algebra.

Lemma minus_trans_not_in :
 forall (A : part_set E) (x y : E),
 ~ in_part y A -> ~ in_part y (minus_part A x).
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, minus_part, diff, single in |- *; simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.
Hint Resolve minus_trans_not_in: algebra.
(*
	Some lemmas.
*)

Lemma union_unit_l : forall A : part_set E, Equal (union (empty E) A) A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, union, empty in |- *; simpl in |- *.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
Qed.
Hint Resolve union_unit_l: algebra.

Lemma single_add : forall x : E, Equal (single x) (add_part (empty E) x).
(* Goal: forall x : Carrier E, @Equal (part_set E) (@single E x) (add_part (empty E) x) *)
unfold add_part in |- *.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
Qed.
Hint Resolve single_add: algebra.

Lemma minus_add :
 forall (A : part_set E) (x : E),
 in_part x A -> Equal (add_part (minus_part A x) x) A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
unfold eq_part, add_part, minus_part, union, diff, single in |- *;
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
 simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
(* Goal: a x0 *)
(* Goal: or (and (a x0) (forall _ : @Equal E x0 x, False)) (@Equal E x0 x) *)
apply pa with x; auto with algebra.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
apply NNPP; intuition.
Qed.
Hint Resolve minus_add: algebra.

Lemma add_minus :
 forall (A : part_set E) (x : E),
 ~ in_part x A -> Equal (minus_part (add_part A x) x) A.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
unfold eq_part, add_part, minus_part, union, diff, single in |- *;
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
 simpl in |- *.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
(* Goal: False *)
apply H.
(* Goal: a x *)
apply pa with x0; auto with algebra.
Qed.
Hint Resolve add_minus: algebra.
(*
	Cardinal.
*)

Inductive cardinal : part_set E -> nat -> Prop :=
  | cardinal_empty : forall A : part_set E, Equal A (empty E) -> cardinal A 0
  | cardinal_add :
      forall (A B : part_set E) (n : nat),
      cardinal B n ->
      forall x : E,
      ~ in_part x B -> Equal A (add_part B x) -> cardinal A (S n).
Hint Immediate cardinal_empty: algebra.

Lemma cardinal_comp :
 forall (A B : part_set E) (n m : nat),
 Equal A B -> n = m -> cardinal A n -> cardinal B m.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
inversion H1.
(* Goal: cardinal B m *)
rewrite <- H0.
(* Goal: cardinal B n *)
(* Goal: cardinal B m *)
rewrite <- H4.
(* Goal: cardinal B O *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
apply cardinal_empty.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
(* Goal: cardinal B m *)
rewrite <- H0.
(* Goal: cardinal B n *)
rewrite <- H6.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_add with B0 x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
Qed.
Hint Resolve cardinal_comp: algebra.

Lemma cardinal_comp_l :
 forall (A B : part_set E) (n : nat),
 Equal A B -> cardinal A n -> cardinal B n.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_comp with A n; auto with algebra.
Qed.

Lemma cardinal_comp_r :
 forall (A : part_set E) (n m : nat), n = m -> cardinal A n -> cardinal A m.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_comp with A n; auto with algebra.
Qed.

Lemma cardinal_empty_O : cardinal (empty E) 0.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
Qed.
Hint Resolve cardinal_empty_O: algebra.

Lemma cardinal_single : forall x : E, cardinal (single x) 1.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
intro.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_add with (empty E) x; auto with algebra.
Qed.
Hint Resolve cardinal_single: algebra.

Lemma cardinal_pair :
 forall x y : E, ~ Equal x y -> cardinal (union (single x) (single y)) 2.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_add with (single x) y; auto with algebra.
Qed.
Hint Resolve cardinal_pair: algebra.

Lemma cardinal_O_empty :
 forall A : part_set E, cardinal A 0 -> Equal A (empty E).
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal (part_set E) A (@single E x)) *)
inversion H.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
Qed.
Hint Resolve cardinal_O_empty: algebra.

Lemma cardinal_1_single :
 forall A : part_set E, cardinal A 1 -> exists x : E, Equal A (single x).
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal (part_set E) A (@single E x)) *)
inversion H.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @Equal (part_set E) A (@single E x)) *)
exists x.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part B x); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part (empty E) x); auto with algebra.
Qed.
(*
	Some lemmas.
*)

Lemma not_in_empty :
 forall A : part_set E, (forall x : E, ~ in_part x A) -> Equal A (empty E).
(* Goal: forall (A : Carrier (part_set E)) (_ : forall x : Carrier E, not (@in_part E x A)), @Equal (part_set E) A (empty E) *)
intros A.
(* Goal: forall _ : forall x : Carrier E, not (@in_part E x A), @Equal (part_set E) A (empty E) *)
case A.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
intros a pa.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part, empty in |- *; simpl in |- *.
(* Goal: forall (_ : forall x : Carrier E, not (a x)) (x : Carrier E), and (forall _ : a x, False) (forall _ : False, a x) *)
intuition eauto.
Qed.
Hint Immediate not_in_empty: algebra.

Lemma not_in_part_trans :
 forall (x : E) (A B : part_set E),
 ~ in_part x A -> Equal A B -> ~ in_part x B.
(* Goal: forall (x y : Carrier E) (A : Carrier (part_set E)) (_ : not (@in_part E x A)) (_ : @Equal E x y), not (@in_part E y A) *)
unfold in_part in |- *.
(* Goal: forall (x : Carrier E) (A B : Carrier (part_set E)) (_ : not (@Pred_fun E A x)) (_ : @Equal (part_set E) A B), not (@Pred_fun E B x) *)
intros x A B.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
case A; case B; simpl in |- *.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (Pred_fun0 : forall _ : Carrier E, Prop) (Pred_compatible_prf0 : @pred_compatible E Pred_fun0) (_ : not (Pred_fun0 x)) (_ : @eq_part E (@Build_Predicate E Pred_fun0 Pred_compatible_prf0) (@Build_Predicate E Pred_fun Pred_compatible_prf)), not (Pred_fun x) *)
intros a pa b pb.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
unfold eq_part in |- *; simpl in |- *.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (H0 x); auto with algebra.
Qed.

Lemma not_in_part_trans_eq :
 forall (x y : E) (A : part_set E),
 ~ in_part x A -> Equal x y -> ~ in_part y A.
(* Goal: forall (x y : Carrier E) (A : Carrier (part_set E)) (_ : not (@in_part E x A)) (_ : @Equal E x y), not (@in_part E y A) *)
unfold in_part in |- *.
(* Goal: forall (x y : Carrier E) (A : Carrier (part_set E)) (_ : not (@Pred_fun E A x)) (_ : @Equal E x y), not (@Pred_fun E A y) *)
intros x y A.
(* Goal: forall (Pred_fun : forall _ : Carrier E, Prop) (Pred_compatible_prf : @pred_compatible E Pred_fun) (_ : forall x : Carrier E, not (@in_part E x (@Build_Predicate E Pred_fun Pred_compatible_prf))), @Equal (part_set E) (@Build_Predicate E Pred_fun Pred_compatible_prf) (empty E) *)
case A; intros a pa.
(* Goal: forall (_ : not (@Pred_fun E (@Build_Predicate E a pa) x)) (_ : @Equal E x y), not (@Pred_fun E (@Build_Predicate E a pa) y) *)
simpl in |- *.
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
(* Goal: False *)
apply H.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply (pa y x); auto with algebra.
Qed.

Lemma cardinal_sup3 :
 forall (A B C : part_set E) (x y : E),
 Equal A (add_part B x) ->
 Equal A (add_part C y) ->
 ~ in_part x B ->
 ~ in_part y C ->
 ~ Equal x y ->
 exists D : part_set E,
   Equal B (add_part D y) /\
   Equal C (add_part D x) /\ ~ in_part x D /\ ~ in_part y D.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @ex (Carrier (part_set E)) (fun D : Carrier (part_set E) => and (@Equal (part_set E) B (add_part D y)) (and (@Equal (part_set E) C (add_part D x)) (and (not (@in_part E x D)) (not (@in_part E y D))))) *)
exists (minus_part B y).
(* Goal: and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y))) *)
split.
(* Goal: @Equal (part_set E) B (add_part (minus_part B y) y) *)
(* Goal: and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y))) *)
apply Sym.
(* Goal: @Equal (part_set E) (add_part (minus_part B y) y) B *)
(* Goal: and (@Equal (part_set E) C (add_part (minus_part B y) x)) (and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y)))) *)
apply minus_add.
(* Goal: @in_part E y B *)
(* Goal: and (@Equal (part_set E) C (add_part (minus_part B y) x)) (and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y)))) *)
cut (in_part y (add_part B x)).
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_in_el_diff with x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part C y); auto with algebra.
(* Goal: and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y))) *)
split.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_simpl with y; auto with algebra.
(* Goal: forall x : Carrier E, cardinal (@single E x) (S O) *)
unfold not in |- *; intro.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
absurd (Equal y x); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_in_el_not_in with (minus_part B y); auto with algebra.
apply Trans with (add_part (add_part (minus_part B y) y) x);
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
 auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part B x); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_comp; auto with algebra.
(* Goal: @Equal (part_set E) B (add_part (minus_part B y) y) *)
(* Goal: and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y))) *)
apply Sym.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply minus_add; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_in_el_diff with x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part C y); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
(* Goal: and (not (@in_part E x (minus_part B y))) (not (@in_part E y (minus_part B y))) *)
split.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply minus_trans_not_in; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
Qed.

Lemma cardinal_ind2 :
 forall P : forall (n : nat) (A : part_set E), cardinal A n -> Prop,
 (forall (A : part_set E) (c : cardinal A 0), P 0 A c) ->
 (forall n : nat,
  (forall (B : part_set E) (c : cardinal B n), P n B c) ->
  forall (A B : part_set E) (x : E),
  ~ in_part x B ->
  Equal A (add_part B x) -> forall c' : cardinal A (S n), P (S n) A c') ->
 forall (n : nat) (A : part_set E) (c : cardinal A n), P n A c.
(* Goal: forall (n : nat) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n *)
simple induction n.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: P (S n0) A c *)
inversion c.
(* Goal: P (S n0) A c *)
apply (H0 n0 H1 A B x H4 H6 c).
Qed.

Lemma cardinal_S :
 forall (n : nat) (A B : part_set E) (x : E),
 ~ in_part x B -> Equal A (add_part B x) -> cardinal A (S n) -> cardinal B n.
(* Goal: forall (n : nat) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n *)
simple induction n.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: cardinal B O *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
apply cardinal_empty.
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
inversion H1.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (classic (Equal x0 x)); intros.
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
apply Trans with B0.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_simpl with x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply not_in_part_trans_eq with x0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part B0 x0); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
(* Goal: @Equal (part_set E) B (empty E) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
absurd (in_part x (single x0)).
(* Goal: not (@in_part E x (@single E x0)) *)
(* Goal: @in_part E x (@single E x0) *)
(* Goal: forall (n : nat) (_ : forall (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)), cardinal B n) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S (S n))), cardinal B (S n) *)
intuition.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part B0 x0); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part B x); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part (empty E) x0); auto with algebra.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: cardinal B (S n0) *)
inversion H2.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (classic (Equal x x0)); intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_comp_l with B0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply add_part_simpl with x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply not_in_part_trans_eq with x0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply Trans with (add_part B0 x0); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim (cardinal_sup3 (A:=A) (B:=B) (C:=B0) (x:=x) (y:=x0)); auto with algebra.
(* Goal: forall (x1 : Carrier (part_set E)) (_ : and (@Equal (part_set E) B (add_part x1 x0)) (and (@Equal (part_set E) B0 (add_part x1 x)) (and (not (@in_part E x x1)) (not (@in_part E x0 x1))))), cardinal B (S n0) *)
intros C H9.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim H9; clear H9; intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim H10; clear H10; intros.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
elim H11; clear H11; intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_add with C x0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply H with B0 x; auto with algebra.
Qed.

Lemma cardinalO_unique :
 forall A : part_set E, cardinal A 0 -> forall m : nat, cardinal A m -> 0 = m.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
inversion H0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
absurd (in_part x (empty E)); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with A; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part B x); auto with algebra.
Qed.

Lemma cardinal_unique :
 forall (n : nat) (A : part_set E),
 cardinal A n -> forall m : nat, cardinal A m -> n = m.
(* Goal: forall (n : nat) (A : Carrier (part_set E)) (_ : cardinal A n) (m : nat) (_ : cardinal A m), @eq nat n m *)
intros n A c.
apply
 cardinal_ind2
  with
    (P := fun (n : nat) (A : part_set E) (c : cardinal A n) =>
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
          forall m : nat, cardinal A m -> n = m); auto with algebra.
(* Goal: forall (A : Carrier (part_set E)) (_ : cardinal A O) (m : nat) (_ : cardinal A m), @eq nat O m *)
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : cardinal B n) (m : nat) (_ : cardinal B m), @eq nat n m) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)) (m : nat) (_ : cardinal A m), @eq nat (S n) m *)
exact cardinalO_unique.
(* Goal: forall (n : nat) (_ : forall (B : Carrier (part_set E)) (_ : cardinal B n) (m : nat) (_ : cardinal B m), @eq nat n m) (A B : Carrier (part_set E)) (x : Carrier E) (_ : not (@in_part E x B)) (_ : @Equal (part_set E) A (add_part B x)) (_ : cardinal A (S n)) (m : nat) (_ : cardinal A m), @eq nat (S n) m *)
intros n0 H A0 B x H0 H1 c' m.
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
case m; intros.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
absurd (in_part x (empty E)); auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with A0; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply in_part_comp_r with (add_part B x); auto with algebra.
(* Goal: @eq nat (S n0) (S n1) *)
cut (cardinal B n0).
(* Goal: forall _ : cardinal B n0, @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n0 *)
cut (cardinal B n1).
(* Goal: forall (_ : cardinal B n1) (_ : cardinal B n0), @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
intros.
(* Goal: @eq nat (S n0) (S n1) *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
cut (n0 = n1).
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply H with B; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_S with A0 x; auto with algebra.
(* Goal: forall _ : @eq nat n0 n1, @eq nat (S n0) (S n1) *)
(* Goal: @eq nat n0 n1 *)
(* Goal: cardinal B n1 *)
(* Goal: cardinal B n0 *)
apply cardinal_S with A0 x; auto with algebra.
Qed.
(* OUF! *)
End fparts_in_def.
Hint Resolve single_law add_part_comp add_part_in add_in minus_part_comp
  minus_part_not_in minus_not_in minus_trans_not_in union_unit_l single_add
  minus_add add_minus cardinal_comp cardinal_empty_O cardinal_single
  cardinal_pair cardinal_O_empty: algebra.
Hint Immediate single_prop: algebra.
Hint Immediate single_prop_rev: algebra.
Hint Immediate add_part_com: algebra.
Hint Immediate minus_part_com: algebra.
Hint Immediate cardinal_empty: algebra.
Hint Immediate not_in_empty: algebra.
