proposition: Lemma BZopp_positive2 x: inc x BZp -> inc (BZopp x) BZm.
proof: Proof. case:(equal_or_not x \0z); first by move => -> _; rewrite BZopp_0; apply:ZmS0. by move => pa pb;apply /setU1_P; left; apply BZopp_positive1; apply /BZps_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)