proposition: Lemma order_exten r r': order r -> order r' -> (forall x y, gle r x y <-> gle r' x y) -> (r = r').
proof: Proof. by move=> or or'; apply: sgraph_exten; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)