proposition: 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.
proof: Proof. simple induction n. auto with algebra. intros. inversion c. apply (H0 n0 H1 A B x H4 H6 c). Qed.
imports: Union Singleton Diff Classical_Prop