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