proposition: 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.
proof: Proof. simple induction n. intros. apply cardinal_empty. inversion H1. elim (classic (Equal x0 x)); intros. apply Trans with B0. apply add_part_simpl with x; auto with algebra. apply not_in_part_trans_eq with x0; auto with algebra. apply Trans with A; auto with algebra. apply Trans with (add_part B0 x0); auto with algebra. auto with algebra. absurd (in_part x (single x0)). intuition. apply in_part_comp_r with (add_part B0 x0); auto with algebra. apply in_part_comp_r with A; auto with algebra. apply in_part_comp_r with (add_part B x); auto with algebra. apply Trans with (add_part (empty E) x0); auto with algebra. intros. inversion H2. elim (classic (Equal x x0)); intros. apply cardinal_comp_l with B0; auto with algebra. apply add_part_simpl with x; auto with algebra. apply not_in_part_trans_eq with x0; auto with algebra. apply Trans with A; auto with algebra. apply Trans with (add_part B0 x0); auto with algebra. elim (cardinal_sup3 (A:=A) (B:=B) (C:=B0) (x:=x) (y:=x0)); auto with algebra. intros C H9. elim H9; clear H9; intros. elim H10; clear H10; intros. elim H11; clear H11; intros. apply cardinal_add with C x0; auto with algebra. apply H with B0 x; auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop