proposition: Lemma BZ_of_Z_prod x y: BZ_of_Z (x * y) = (BZ_of_Z x) *z (BZ_of_Z y).
proof: Proof. have ppc:forall n m: nat, BZ_of_Z (Posz n * Posz m) = BZ_of_Z n *z BZ_of_Z m. move => n m; move: (positive_non_zero1 n)(positive_non_zero1 m) => pa pb. by simpl;rewrite (BZprod_pp pa pb) !BZ_of_nat_val nat_to_B_prod. have npc: forall n (m:nat), BZ_of_Z (Posz m * Negz n) = BZ_of_Z m *z BZ_of_Z (Negz n). move => n m; rewrite BZ_of_Z_neg - BZopp_prod_r;try apply:BZ_of_Z_inc. by rewrite - ppc NegzE mulrN BZ_of_Z_opp. move; case: x; case: y => n m. - by apply: ppc. - apply: npc. - rewrite BZprodC mulrC; apply: npc. - move: (positive_non_zero2bis n)(positive_non_zero2bis m) => pa pb. rewrite (BZprod_mm pb pa) ! BZm_of_nat_val - nat_to_B_prod //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)