proposition: Lemma BZopp_sg x: intp x -> x <> \0z -> ((int_np x -> int_pp (BZopp x)) /\ (int_pp x -> int_np (BZopp x))).
proof: Proof. move => pa pb; rewrite /int_np /int_pp. have pnz: (P x <> \0c) by move => h; case: pb; apply: BZ_0_if_val0. by rewrite /BZopp /BZ_of_nat /BZm_of_nat; Ytac0;Ytac sx; aw; rewrite ? sx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)