proposition: Lemma cardinal_no_inj_equiv_lt_cardinal (A B : Type) : (forall f : A -> B, ~ injective f) <-> lt_cardinal B A.
proof: Proof. split. - intros. split. + destruct (le_cardinal_total B A). { assumption. } destruct H0 as [f Hf]. specialize (H f Hf). contradiction. + intro. destruct H0 as [f Hf]. apply bijective_impl_invertible in Hf. destruct Hf as [g Hgf Hfg]. pose proof (invertible_impl_bijective g). destruct H0 as [Hg0 Hg1]. { exists f; assumption. } apply (H g Hg0). - intros [[f Hf]] g Hg. contradict H. apply CSB with (f := f) (g := g); assumption. Qed.
imports: Coq(ClassicalChoice) Coq(ProofIrrelevance) Coq(FunctionalExtensionality) Coq(Description) ZornsLemma(FunctionPropertiesEns) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(CSB) ZornsLemma(EnsemblesSpec) ZornsLemma(ZornsLemma) ZornsLemma(EnsemblesImplicit) ZornsLemma(CountableTypes) ZornsLemma(FiniteTypes) ZornsLemma(InfiniteTypes) Coq(RelationClasses)