proposition: Lemma zle_opp x y: x <=z y -> (BZopp y) <=z (BZopp x).
proof: Proof. move => leq; move: (leq) => [xz yz etc]. case: (equal_or_not x \0z) => xnz. move: leq; rewrite xnz => /zle0xP yp; rewrite BZopp_0. by apply/zge0xP; apply: BZopp_positive2. case: (equal_or_not y \0z) => ynz. move: leq; rewrite ynz => /zge0xP yp;rewrite BZopp_0. by apply/zle0xP; apply: BZopp_negative2. move: (ZSo xz) (ZSo yz) => x'z y'z. split => //; rewrite (BZopp_val x) (BZopp_val y). move: (BZopp_sg xz xnz) (BZopp_sg yz ynz) => [qa qb][qc qd]. case: etc. - move => [pa pb pc]; constructor 3; split; fprops. - move => [pa pb];constructor 2; split; fprops. - by move => [pa pb pc]; constructor 1; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)