proposition: Lemma zle_oppP x y: intp x -> intp y -> (BZopp y <=z BZopp x <-> x <=z y).
proof: Proof. move => pa pb; split; last by apply: zle_opp. by move=> h; move: (zle_opp h); rewrite (BZopp_K pa) (BZopp_K pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)