proposition: Lemma preorderP g: sgraph g -> (preorder g <-> (sub (diagonal (substrate g)) g /\ sub (g \cg g) g)).
proof: Proof. move=> gg;split. move=> [_ rr tr]; split; move=> x. by move/diagonal_i_P=> [px Px pq]; rewrite -px -pq; apply: rr. move: tr;rewrite idempotent_graph_transitive //; apply. move=> [s1 s2];split=> //. by move=> y ys; apply: s1; apply/diagonal_pi_P. by rewrite idempotent_graph_transitive. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)