proposition: Lemma le_cardinal_total: forall kappa lambda:Cardinal, le_cardinal kappa lambda \/ le_cardinal lambda kappa.
proof: Proof. intros. destruct kappa. destruct lambda. pose proof (types_comparable T T0). case H. left. destruct H0. exists x. assumption. right. destruct H0. exists x. assumption. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice ZornsLemma EnsemblesImplicit ProofIrrelevance FunctionalExtensionality Description