proposition: Lemma BZprod_mp x y: inc x BZms -> inc y BZp -> x *z y = BZm_of_nat ((BZ_val x) *c (BZ_val y)).
proof: Proof. by move => pa pb; rewrite BZprodC;rewrite BZprod_pm // cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)