proposition: Lemma rle_opp_iso: order_isomorphism (Lf BRopp BR BR) BR_order (opp_order BR_order).
proof: Proof. move: BR_osr BRopp_fb => [or sr] bf. have la: lf_axiom BRopp BR BR by move => t tr;apply:RSo. have [pa pb]:= (opp_osr or). hnf;rewrite pb; aw;split => //; first by saw. hnf; aw;move => x y xr yr; rewrite ! LfV//;split. by move /BR_gleP => h; apply /opp_gleP; apply /BR_gleP; apply rle_opp. move /opp_gleP /BR_gleP => h; apply /BR_gleP. by rewrite - (BRopp_K xr) -(BRopp_K yr); apply rle_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)