proposition: Lemma graph_on_P0 r x a b: inc (J a b) (graph_on r x) <-> [/\ inc a x, inc b x & r a b].
proof: Proof. split; first by move/Zo_P => [] /setX_P; aw ; move => [pa pb pc] pd;split. by move => [pa pb pc]; apply: Zo_i; [apply: setXp_i | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)