proposition: Lemma Countable_as_le_cardinal_ens {X : Type} (U : Ensemble X) : Countable U <-> le_cardinal_ens U (@Full_set nat).
proof: Proof. split. - intros [f Hf]. pose proof (eq_cardinal_ens_sig U). eapply le_cardinal_ens_Proper_l; eauto. right. exists f. split; [|firstorder]. intros ? ?. constructor. - intros [[]|[f [_ Hf]]]. { contradict (H 0). } exists (fun p => f (proj1_sig p)). intros [x0 H0] [x1 H1] Hx. simpl in Hx. specialize (Hf x0 x1 H0 H1 Hx). apply subset_eq_compat. 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)