proposition: Lemma least_cardinal_unique P {X : Type} (U : Ensemble X) {Y : Type} (V : Ensemble Y) : least_cardinal P U -> least_cardinal P V -> eq_cardinal_ens U V.
proof: Proof. intros [HU0 HU1] [HV0 HV1]. specialize (HU1 Y V HV0). specialize (HV1 X U HU0). apply le_cardinal_ens_antisymmetry; 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)