proposition: Lemma least_cardinal_ext_to_subset {X : Type} (P : Family X) {Y : Type} (V : Ensemble Y) : least_cardinal_ext P V -> exists U : Ensemble X, least_cardinal_subset P U /\ eq_cardinal_ens U V.
proof: Proof. intros [[U [HU0 HU1]] HV1]. exists U. split; auto. split; auto. intros W HW. apply eq_cardinal_ens_sym in HU1. eapply le_cardinal_ens_Proper_l; eauto. apply HV1. exists W; split; auto. reflexivity. 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)