proposition: Lemma BZprod_pm x y: inc x BZp -> inc y BZms-> x *z y = BZm_of_nat ((BZ_val x) *c (BZ_val y)).
proof: Proof. move => pa pb; rewrite BZprodE /BZprod_int (BZp_sg pa)(BZms_sg pb). by Ytac0;rewrite /BZopp /BZ_of_nat /int_np pr2_pair; Ytac0; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)