proposition: Lemma p2graph_target1 x: inc x (graph f) -> inc (Q x) (target f).
proof: Proof. move=> xgf; rewrite (in_graph_Vf xgf); aw. by apply: Vf_target => //; apply: p1graph_source1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)