proposition: Lemma BZprod_abs2 x y: intp x -> intp y -> x *z y = J ((BZ_val x) *c (BZ_val y)) (BZprod_sign_aux x y).
proof: Proof. move => xz yz; rewrite /BZprod_sign_aux. case: (equal_or_not x \0z). by move => ->;rewrite BZprod_0l BZ0_val cprod0l; Ytac0. move=> xnz;case: (equal_or_not y \0z). by move => ->;rewrite BZprod_0r BZ0_val cprod0r; Ytac0; Ytac0. move => ynz; Ytac0; Ytac0. move:(BZprod_nz xz yz xnz ynz). rewrite BZprodE /BZprod_int ; Ytac qxy; Ytac0 => //. rewrite /BZopp /BZ_of_nat/ int_np; aw; Ytac0. by rewrite /BZm_of_nat; Ytac ww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)