proposition: Lemma gfunctions_i f: function f -> inc (graph f) (gfunctions (source f) (target f)).
proof: Proof. by move=> [[pa pd] pb pc]; apply: Zo_i => //; apply/setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)