proposition: Lemma qle_opp_iso: order_isomorphism (Lf BQopp BQ BQ) BQ_order (opp_order BQ_order).
proof: Proof. move: BQor_or BQor_sr BQopp_fb => or sr bf. have la: lf_axiom BQopp BQ BQ by move => t tz; apply:QSo. move: (opp_osr or) => [pa pb]. hnf;rewrite pb; saw; first by saw. hnf; aw;move => x y xz yz; rewrite !LfV//; split. by move /BQle_P => h; apply /opp_gleP; apply /BQle_P;apply qle_opp. move /opp_gleP /BQle_P => h; apply /BQle_P. by rewrite - (BQopp_K xz) -(BQopp_K yz); apply qle_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)