proposition: Lemma surjective_pr0 f: surjection f -> Imf f = target f.
proof: Proof. move=> [ff sj]; apply: extensionality; first by apply:(Imf_Starget ff). move => t tf; move: (sj _ tf) => [x xsf ->]. apply/dirim_P; ex_tac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)