proposition: Lemma bijective_if_same_finite_c_surj f: cardinal (source f) = cardinal (target f) -> finite_set (source f) -> surjection f -> bijection f.
proof: Proof. move=> cstf fsf sf. move: (exists_right_inv_from_surj sf)=> [g rig]. move: (right_i_source rig) =>sg. move: (right_inverse_fi rig)=> ig. move: rig =>[co c]; move: (co) => [_ s t]. have csftf: (cardinal (source g) = cardinal (target g)) by rewrite sg -t. have fss: finite_set (source g) by hnf; rewrite sg - cstf. have bg :=(bijective_if_same_finite_c_inj csftf fss ig). have bc: (bijection (compose f g)) by rewrite c; apply: identity_fb. apply: (left_compose_fb co bc bg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)