proposition: Lemma order_from_rel1 r x: transitive_r r -> (forall u v, inc u x -> inc v x -> r u v -> r v u -> u = v) -> (forall u, inc u x -> r u u) -> order (graph_on r x).
proof: Proof. move=> tr sy re. have ->: (graph_on r x = graph_on (fun a b => [/\ inc a x, inc b x & r a b]) x). by apply: Zo_exten1 => t /setX_P [_ px qx]; split => // [] [_ _]. apply: order_from_rel; split. + by move => a b c [ax bx rab] [_ cx rbc]; split => //; apply: tr rab rbc. + by move=> a b [ax bx rab] [_ cx rbc]; apply: sy. + by move=> a b [ax bx rab];split => //; split => //; apply: re. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)