proposition: Lemma BZnon_zero_opp x: intp x -> (x <> \0z <-> BZopp x <> \0z).
proof: Proof. move => xz;apply:iff_neg; split => h; first by rewrite h BZopp_0. by apply: (BZ_0_if_val0 xz); rewrite - (BZopp_val x) h BZ0_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)