proposition: Lemma card_le_surj a b : a <=cc b -> nonempty a -> exists f, surjection_prop f b a.
proof: Proof. move => /eq_subset_cardP1 [f [fi <- tf]] nes. move: (exists_left_inv_from_inj fi nes) => [g gp]; exists g; hnf. rewrite (left_i_source gp) (left_i_target gp). split => //; apply: (left_inverse_fs gp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)