proposition: Lemma toZp_shlBn: forall n (p: BITS n) k, k < n -> toZp (shlBn p k) = (toZp p * (2 ^ k)%:R)%R.
proof: Proof. move=> n p. elim=> [|k IHk] le_k. + by rewrite expn0 GRing.mulr_natr //. + rewrite /shlBn iterS -[iter k shlB p]/(shlBn _ _). rewrite toZp_shlB. rewrite IHk; last by auto with arith. by rewrite expnS mulnC !GRing.mulr_natr GRing.mulrnA. 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)