proposition: Lemma zlt_opp x y: x <z y -> (BZopp y) <z (BZopp x).
proof: Proof. move => [pa pb]; split; first by apply:zle_opp. by move: pa => [xz yz _] pc; case: pb; apply:BZopp_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)