proposition: Lemma idempotent_graph_transitive r: sgraph r -> (transitivep r <-> sub (r \cg r) r).
proof: Proof. move=> gr; split. move=> tr t /compg_P [pt [y J1r J2r]]. rewrite - pt; move: tr J1r J2r; apply. by move => h x y z Jxy Jyz; apply: h; apply/compg_pP; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)