proposition: Lemma incl_card_le : forall (X Y:Ensemble U) (n m:nat), cardinal U X n -> cardinal U Y m -> Included U X Y -> n <= m.
proof: Proof. intros X Y n m HX HY HXY. destruct (Included_Strict_Included _ _ _ HXY) as [HXY' | <-]. - apply Nat.lt_le_incl. now apply (incl_st_card_lt _ _ HX _ _ HY). - apply Nat.eq_le_incl. now apply cardinal_unicity with X. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat