proposition: Lemma le_lt_cardinal_ens_transitive {X Y Z : Type} (U : Ensemble X) (V : Ensemble Y) (W : Ensemble Z) : le_cardinal_ens U V -> lt_cardinal_ens V W -> lt_cardinal_ens U W.
proof: Proof. intros HUV [HVW HVWn]. split. { eapply le_cardinal_ens_transitive; eauto. } intros Heq. contradict HVWn. apply eq_cardinal_ens_sym in Heq. apply le_cardinal_ens_antisymmetry; auto. eapply le_cardinal_ens_Proper_l; eauto. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)