proposition: Lemma surjectionsP E F f: inc f (surjections E F) <-> surjection_prop f E F.
proof: Proof. split; first by by move => /Zo_P [/functionsP [ha hb hc] hd]. move => [ha hb hc]; apply: Zo_i => //; apply/functionsP; split => //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)