proposition: Lemma preorder_from_rel r x: preorder_r r -> preorder (graph_on r x).
proof: Proof. move=> pr. have gg: sgraph (graph_on r x) by apply: graph_on_graph. move: pr=> [tr rr]. split=>//. by move=> y /(substrate_P gg) [] [z] /graph_on_P0 [yx zx ryz]; apply /graph_on_P0; split => // ;move: (rr _ _ ryz) => []. move=> a b c /graph_on_P1 [ax bx rab] /graph_on_P1 [_ cx rbc]. apply /graph_on_P1;split => //; apply: tr rab rbc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)