proposition: Lemma BZopp_prod_r x y: intp x -> intp y -> BZopp (x *z y) = x *z (BZopp y).
proof: Proof. move => pa pb. case /BZ_i1P: (pa). + by move => ->; rewrite !BZprod_0l BZopp_0. + move => h1; case /BZ_i1P: pb => h2. - by rewrite h2 BZopp_0 !BZprod_0r BZopp_0. - move:(BZps_sBZp h1) => h3. rewrite (BZprod_pp h3 (BZps_sBZp h2)). by rewrite(BZprod_pm h3 (BZopp_positive1 h2)) BZopp_val BZopp_p. - rewrite (BZprod_pm (BZps_sBZp h1) h2). rewrite (BZprod_pp (BZps_sBZp h1) (BZps_sBZp (BZopp_negative1 h2))). by rewrite BZopp_val BZopp_m. + move => h1; case /BZ_i1P: pb => h2. - by rewrite h2 BZopp_0 !BZprod_0r BZopp_0. - rewrite(BZprod_mp h1 (BZps_sBZp h2)). by rewrite (BZprod_mm h1 (BZopp_positive1 h2)) BZopp_val BZopp_m. - rewrite (BZprod_mm h1 h2) (BZprod_mp h1 (BZps_sBZp (BZopp_negative1 h2))). by rewrite BZopp_val BZopp_p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)