proposition: Lemma surj_le_cardinal: forall {X Y:Type} (f:X->Y), surjective f -> le_cardinal (cardinality Y) (cardinality X).
proof: Proof. intros. pose proof (choice (fun (y:Y) (x:X) => f x = y) H). simpl in H0. destruct H0 as [g]. exists g. red; intros. congruence. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice