proposition: Lemma incl_st_card_lt : forall (X:Ensemble U) (c1:nat), cardinal U X c1 -> forall (Y:Ensemble U) (c2:nat), cardinal U Y c2 -> Strict_Included U X Y -> c2 > c1.
proof: Proof. intros X c1 H1. induction H1 as [|X' ? HX' IH x Hx]; intros Y c2 HY Hsincl; (inversion HY as [HXY Hc | ? ? ? ? ? HXY]; subst Y; [ apply not_SIncl_empty in Hsincl as [] |]). - apply Nat.lt_0_succ. - subst c2. apply -> Nat.succ_lt_mono. refine (IH _ _ _ (incl_st_add_soustr _ _ _ _ Hx Hsincl)). rewrite <- Nat.pred_succ. apply card_soustr_1; [ assumption | ]. apply Hsincl, Add_intro2. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat