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