proposition: Lemma bijective_if_same_finite_c_inj f: cardinal (source f) = cardinal (target f) -> finite_set (source f) -> injection f -> bijection f.
proof: Proof. move=> csftf fs injf; split=>//; apply: surjective_pr1; first by fct_tac. have fst: (finite_set (target f)) by hnf; ue. have sit: (sub (Imf f) (target f)) by apply: Imf_Starget; fct_tac. by apply:(strict_sub_smaller_contra fst sit); rewrite (cardinal_range injf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)