proposition: Lemma card_soustr_1 : forall (X:Ensemble U) (n:nat), cardinal U X n -> forall x:U, In U X x -> cardinal U (Subtract U X x) (pred n).
proof: Proof. intros X n H. induction H as [|X n H IH x Hx]; intros x' Hx'. - destruct Hx'. - rewrite Nat.pred_succ. apply Add_inv in Hx' as [Hx' | <-]. + rewrite (add_soustr_xy _ _ x x') by (intros <-; contradiction Hx). rewrite <- Nat.succ_pred_pos. * apply card_add; [ apply (IH _ Hx') |]. now intros [? _]%Subtract_inv. * apply inh_card_gt_O with (X := X); [| assumption ]. exact (Inhabited_intro _ _ _ Hx'). + rewrite <- (Sub_Add_new _ _ _ Hx). assumption. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat