proposition: Corollary le_cardinal_total: forall kappa lambda:Type, le_cardinal kappa lambda \/ le_cardinal lambda kappa.
proof: Proof. intros T0 T1. destruct (types_comparable T0 T1) as [[f]|[f]]; [left|right]; exists f; 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)