proposition: Lemma OT_opposite1 a b: a \Is b -> (opp_order a) \Is (opp_order b).
proof: Proof. move=> [f [o1 o2 bp isf]]. move: (opp_osr o1)(opp_osr o2) => [pa pb][pc pd]. exists f;split => //;fprops; rewrite ? pb ? pd //. move=> x y asf bsf. by split; move /opp_gleP /(isf _ _ bsf asf) /opp_gleP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)