proposition: Lemma cardinal_minus_part : forall (B : part_set F) (x : F) (n : nat), cardinal B (S n) -> in_part x B -> cardinal (diff B (single x)) n.
proof: Proof. intros B x n H' H'0; try assumption. apply cardinal_S with B x; auto with *. unfold not in |- *; intros. cut (~ in_part x (single x)). unfold not in |- *; auto with *. apply diff_in_r with B; auto with *. Qed.
imports: Fpart2