proposition: Corollary le_cardinal_ens_antisymmetry {X Y : Type} (U : Ensemble X) (V : Ensemble Y) : le_cardinal_ens U V -> le_cardinal_ens V U -> eq_cardinal_ens U V.
proof: Proof. intros [H|[f [Hf0 Hf1]]]. { left. assumption. } intros [H|[g [Hg0 Hg1]]]. { apply eq_cardinal_ens_sym. left. assumption. } right. apply (CSB_ens _ _ f g); assumption. 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)