proposition: Lemma BZprodA x y z: intp x -> intp y -> intp z -> x *z (y *z z) = (x *z y) *z z.
proof: Proof. move => pa pb pc; move: (ZSp pa pb) (ZSp pb pc) => pab pbc. rewrite (BZprod_abs2 pa pbc) (BZprod_abs2 pab pc) BZprod_val BZprod_val cprodA. congr (J _ _). rewrite /BZprod_sign_aux. Ytac xz; first by rewrite xz BZprod_0l; Ytac0. case: (equal_or_not y \0z) => yz. by rewrite yz BZprod_0l BZprod_0r; Ytac0; Ytac0. rewrite (Y_false (BZprod_nz pa pb xz yz)). case: (equal_or_not z \0z) => zz; Ytac0; first by rewrite zz BZprod_0r; Ytac0. rewrite (Y_false (BZprod_nz pb pc yz zz)). rewrite (BZprod_abs2 pa pb) (BZprod_abs2 pb pc) ! pr2_pair. rewrite /BZprod_sign_aux; Ytac0; Ytac0; Ytac0; Ytac0. have aux: forall t, inc t BZ -> Q t = C0 \/ Q t = C1. by move => t /candu2P [_]; case; move => [_]; [left | right]. by case /aux: pa => ->; case /aux: pb => ->; case /aux: pc => ->; Ytac0; Ytac0; (try Ytac0) => //; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)