proposition: Lemma BZprod_sign x y: intp x -> intp y -> BZsign (x *z y) = (BZsign x) *z (BZsign y).
proof: Proof. move => xz yz. case:(equal_or_not x \0z) => xnz. by rewrite xnz BZprod_0l BZsign_0 BZprod_0l. case:(equal_or_not y \0z) => ynz. by rewrite ynz BZprod_0r BZsign_0 BZprod_0r. rewrite (BZprod_abs2 xz yz) /BZprod_sign_aux /BZsign/int_pp pr1_pair pr2_pair. have pxnz: (P x) <> \0c by move => h; case: xnz; exact (BZ_0_if_val0 xz h). have pynz: (P y) <> \0c by move => h; case: ynz; exact (BZ_0_if_val0 yz h). move: (cprod2_nz pxnz pynz) => pxynz. Ytac0; Ytac0; Ytac0; Ytac0; Ytac0. move: ZS1 ZSm1 => ha hb. case: (equal_or_not (Q x) (Q y)) => sq; Ytac0; Ytac0. by rewrite - sq; Ytac qa;rewrite ? BZprod_1r // (BZprod_m1r hb) BZopp_m1. move: sq;case /BZ_sgv: xz => ->; Ytac0. case /BZ_sgv: yz => ->; Ytac0 => //; rewrite ? (BZprod_1r ZSm1) //. by case /BZ_sgv: yz => ->; Ytac0 => //; rewrite (BZprod_1l ZSm1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)