proposition: Lemma toNat_fullmulB n1 n2 (p1:BITS n1) (p2: BITS n2) : toNat (fullmulB p1 p2) = (toNat p1 * toNat p2).
proof: Proof. induction n1. rewrite (tuple0 p1)/=. by rewrite !mul0n toNat_fromNat mod0n. case/tupleP: p1 => [b p]. rewrite /=theadCons toNatCons beheadCons. destruct b. + rewrite toNat_addB toNat_joinlsb toNat_joinmsb0 IHn1 add0n toNat_zeroExtendAux. rewrite -!muln2. rewrite mulnDl mul1n addnC -mulnAC. rewrite modn_small => //. rewrite -{1}(mul1n (toNat p2)). rewrite -mulnDl. rewrite expnD. rewrite ltn_mul => //. rewrite expnS. rewrite add1n muln2 mul2n. rewrite ltn_Sdouble. apply (toNatBounded p). apply (toNatBounded p2). by rewrite toNat_joinlsb IHn1 !add0n -!muln2 mulnAC. 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)