proposition: Lemma toZp_shlB n (p: BITS n) : toZp (shlB p) = (toZp p * 2%:R)%R.
proof: Proof. destruct n. by rewrite (tuple0 p). destruct n. case/tupleP: p => [b p]. rewrite (tuple0 p). by destruct b. rewrite /shlB. rewrite toZp_dropmsb /toZpAux. rewrite toNat_shlBaux. rewrite /toZp. apply val_inj. rewrite /=Zp_cast. rewrite (@modn_small 1); last apply pow2_gt1. rewrite (@modn_small (toNat p)); last apply toNatBounded. rewrite addnn. rewrite (@modn_small 1.*2). by rewrite muln2. rewrite expnS mul2n. rewrite ltn_double. apply pow2_gt1. apply pow2_gt1. 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)