proposition: Lemma BZopp_negative1 x: inc x BZms -> inc (BZopp x) BZps.
proof: Proof. move => xn; move : (BZms_sBZ xn) => xz. move: (BZms_nz xn) => xnz ;apply/ BZps_iP; split. exact: (BZp_i (ZSo xz) (proj1 (BZopp_sg xz xnz) (BZms_sg xn))). by apply /(BZnon_zero_opp xz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)