proposition: Lemma BZquo_opp_a1 a b: intp a -> intp b -> b <> \0z -> (BZ_val a) %%c (BZ_val b) = \0c -> (BZopp a) %/z b = BZopp (a %/z b).
proof: Proof. move => az bz bnz de. move: (BZquo_div1 az bz bnz de) => r1. move: de; rewrite -(BZopp_val a) => de. move: (ZS_quo az bz) (ZSo az) => qz naz. move: (BZquo_div1 naz bz bnz de); rewrite {1} r1. rewrite (BZopp_prod_r bz qz) => e1. symmetry;apply: (BZprod_eq2l (ZSo qz) (ZS_quo naz bz) bz bnz e1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)