proposition: Lemma BZrem_opp_b a b: intp a -> intp b -> a %%z (BZopp b) = a %%z b.
proof: Proof. move => az bz; rewrite /BZrem (BZquo_opp_b az bz). by rewrite (BZprod_opp_opp bz (ZS_quo az bz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)