proposition: Lemma surjective_pr5 f: function f -> (forall y, inc y (target f) -> exists2 x, inc x (source f) & related (graph f) x y) -> surjection f.
proof: Proof. move=> ff prop; split => // y yt; move: (prop _ yt) => [x xsf h]; ex_tac. by apply: Vf_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)