proposition: Lemma zle_opp_iso: order_isomorphism (Lf BZopp BZ BZ) BZ_order (opp_order BZ_order).
proof: Proof. move: BZor_or BZor_sr BZopp_fb => or sr bf. have la: lf_axiom BZopp BZ BZ by move => t /ZSo. move: (opp_osr or) => [pa pb]. hnf;rewrite pb /BZopp_fun; aw;split; [exact | fprops | split; aw=> // | ]. hnf; aw;move => x y xz yz; rewrite !LfV //; split. by move /zle_P => h; apply /opp_gleP; apply /zle_P;apply zle_opp. by move /opp_gleP /zle_P /(zle_oppP xz yz) /zle_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)