proposition: Lemma iorder_opposite r x: order r -> commutes_at (induced_order ^~ x) (opp_order) r.
proof: Proof. move => or. apply: sgraph_exten. apply: (setI2_graph2); apply: coarse_graph. apply: igraph_graph. move => u v; split. move /iorder_gleP => [pa pb /igraph_pP pc]. by apply/igraph_pP; apply /iorder_gleP. move/igraph_pP => /iorder_gleP [pa pb pc]. by apply /iorder_gleP;split => //; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)