proposition: Lemma opp_osr r: order r -> order_on (opp_order r) (substrate r).
proof: Proof. move => osr. have go: sgraph (opp_order r) by fprops. have pc: substrate (opp_order r) = (substrate r). set_extens x. case/(substrate_P go) => [][y] /igraph_pP h; substr_tac. by move => xsr; apply /(arg1_sr (y:=x))/igraph_pP /(order_reflexivityP osr). split => //;split; first by fprops. by move => t; rewrite pc => yg; apply/opp_gleP; order_tac. move => x y z /opp_gleP pa /opp_gleP pb; apply/opp_gleP; order_tac. move => x y /opp_gleP pa /opp_gleP pb; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)