proposition: Lemma surjectiveE (rT aT : finType) (f : aT -> rT) : surjective f -> #|codom f| = #|rT|.
proof: Proof. move => H. apply: eq_card => x. rewrite inE. apply/codomP. move: (H x) => [y /eqP]. eauto. Qed.
imports: mathcomp(all_ssreflect)