proposition: Lemma graph_on_P2 r x : equivalence_re r x -> forall u v, (related (graph_on r x) u v <-> r u v).
proof: Proof. move=> [[rs rt] rr] u v; split; first by move/Zo_hi; aw. move => ruv; apply/ graph_on_P1. move: (rs _ _ ruv) => rvu; move: (rt _ _ _ ruv rvu) => ruu. by move: (rt _ _ _ rvu ruv) => rvv; split => //; apply rr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)