proposition: Lemma surj_card_bij (T T' : finType) (f : T -> T') : surjective f -> #|T| = #|T'| -> bijective f.
proof: Proof. move => S E. apply: inj_card_bij; last by rewrite E. apply/injectiveP; apply/card_uniqP. rewrite size_map -cardT E. exact: surjectiveE. Qed.
imports: mathcomp(all_ssreflect)