proposition: Lemma functionsP x y f: inc f (functions x y) <-> (function_prop f x y).
proof: Proof. rewrite/function; split. move/Zo_P => [/correspondences_P [p1 p2 p3] [p4 p5]]; split => //. split => //; ue. by move=> [[qa qb qc] <- pc]; apply: Zo_i; [apply/correspondences_P | split]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)