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