proposition: Lemma BZopp_negative2 x: inc x BZm -> inc (BZopp x) BZp.
proof: Proof. case /setU1_P => h; first by move: (BZopp_negative1 h) => /BZps_iP []. by rewrite h BZopp_0; apply: ZpS0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)