proposition: Theorem le_cardinal_ens_total {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : le_cardinal_ens U V \/ le_cardinal_ens V U.
proof: Proof. destruct (types_comparable (sig U) (sig V)) as [[f Hf]|[f Hf]]; [left|right]. - eapply le_cardinal_ens_sig_injective; eauto. - eapply le_cardinal_ens_sig_injective; 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)