proposition: Lemma preorder_prop1 g: sgraph g -> sub (diagonal (substrate g)) g -> sub (g \cg g) g -> g \cg g = g.
proof: Proof. move=> gg sig scg; apply: extensionality; first by aw. move => x xg; apply /compg_P; split; first by apply: gg. exists (Q x); rewrite ? (gg _ xg) //;apply: sig; apply/diagonal_pi_P. split => //;substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)