proposition: Lemma set_surj_fun_onP (aT rT: finType)(B: {set rT} )(f: {ffun aT -> rT}): reflect ((forall b, b \in B -> exists2 a, a \in aT & b = f a) /\ (forall a, f a \in B)) (f \in set_surj_fun_on aT B).
proof: Proof. rewrite inE; apply: (iffP eqP). move => <-; split;[ by move => b /imsetP | by move => a;apply: imset_f]. move => [h1 h2]; apply /setP => b; apply /idP/idP. move /imsetP => [x] _ ->;apply: h2. by move => bb; apply /imsetP; apply: h1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)