proposition: Lemma set_surj_fun_P (aT rT: finType) (f: {ffun aT -> rT}): reflect (forall b, exists a, b = f a)(f \in set_surj_fun aT rT).
proof: Proof. rewrite inE; apply: (iffP eqP) => h. move => b; have brt: b \in f @: aT by rewrite h. by move /imsetP: brt => [a _ ->]; exists a. apply /setP => b; apply /idP/idP. by move /imsetP; rewrite inE. by move: (h b) => [a -> _]; apply: imset_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)