proposition: Lemma graph_on_P3 r x: order_re r x -> forall u v, (related (graph_on r x) u v <-> r u v).
proof: Proof. move=> [[_ _ cc] rr]; split; first by move /Zo_hi; aw. move => ruv; move: (cc _ _ ruv) => [ruu rvv]. by apply: Zo_i ; [by apply:setXp_i; apply /rr | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)