proposition: Lemma eq_cardinal_impl_le_cardinal: forall kappa lambda: Cardinal, eq_cardinal kappa lambda -> le_cardinal kappa lambda.
proof: Proof. intros. destruct H. exists f. destruct H. assumption. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec