proposition: Lemma shrB_mul2exp m : forall n (p: BITS (m+n)), toNat p < 2^n -> iter m shrB (p *# (2^m)) = p.
proof: Proof. induction m. move => n p H. by rewrite /iter expn0 mulB1. move => n. rewrite (addSn m n). case/tupleP => [b p]. move => H. rewrite iterSr expnS mulB_muln. rewrite -mulBA (mulBC #2) mulBA. specialize (IHm n.+1). rewrite addnS in IHm. specialize (IHm ([tuple of b::p])). rewrite expnS mul2n in IHm. rewrite shrB_mul2. rewrite IHm. done. apply (ltn_trans H). rewrite -muln2. apply ltn_Pmulr => //. apply expn_gt0. rewrite msb0Bounded. rewrite !expnD. rewrite toNat_mulB. rewrite toNatCons. rewrite toNat_fromNat. rewrite (@modn_small (2^m)). rewrite expnS expnD. rewrite toNatCons in H. set BB := b + (toNat p).*2. fold BB in H. rewrite modn_small. rewrite mulnC. rewrite ltn_mul2l. rewrite H andbT. apply expn_gt0. rewrite mulnC. rewrite (mulnC 2 _) -mulnA. rewrite ltn_mul2l. rewrite (expn_gt0 2 m)/=. have: 2^n < 2^n * 2. rewrite ltn_Pmulr => //. apply expn_gt0. by apply (ltn_trans). rewrite expnS expnD mulnCA. rewrite ltn_Pmulr => //. rewrite -expnS. apply pow2_gt1. apply expn_gt0. 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)