proposition: Lemma toZp_mulB n (p1 p2: BITS n) : toZp (mulB p1 p2) = (toZp p1 * toZp p2)%R.
proof: Proof. destruct n. by rewrite (tuple0 p1) (tuple0 p2). rewrite /mulB/toZp. rewrite toNat_low. rewrite toNat_fullmulB. rewrite modZp_pow. rewrite -!Zp_nat. by rewrite !natrM. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)