proposition: Lemma surjective_cle x y: (exists z, surjection_prop z x y) -> y <=cc x.
proof: Proof. move=> [z [sjz sz tz]]. apply /eq_subset_cardP1. move: (exists_right_inv_from_surj sjz) => [f ri]. have ii:=(right_inverse_fi ri). have si:= (right_i_source ri). move: ri=> [[_ _ ti] _]. by rewrite -tz - sz - si ti; exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)