proposition: Lemma eq_cardinal_ens_le {A B : Type} (U : Ensemble A) (V : Ensemble B) : eq_cardinal_ens U V -> le_cardinal_ens U V.
proof: Proof. intros [H|[f [Hf0 [Hf1 _]]]]. { left; auto. } right. exists f; split; auto. 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)