proposition: Lemma toZp_shlBaux n (p: BITS n) : toZp (shlBaux p) = (toZpAux p * 2%:R)%R.
proof: Proof. destruct n. by rewrite (tuple0 p). apply val_inj. rewrite /toZp toNat_shlBaux. rewrite /=Zp_cast; last apply pow2_gt1. rewrite modn_small. rewrite (@modn_small 1); last apply pow2_gt1. rewrite (@modn_small (1+1)). rewrite (@modn_small (toNat p)). rewrite addnn. rewrite muln2. rewrite (@modn_small) => //. rewrite expnS mul2n ltn_double. apply toNatBounded. have B:=toNatBounded p. have: 2^n.+1 <= 2^n.+2. replace (2^n.+2) with (2 * 2^n.+1). apply leq_pmull => //. by rewrite -expnS. apply: leq_trans B. rewrite addnn. rewrite expnS mul2n. rewrite ltn_double. apply pow2_gt1. rewrite expnS mul2n. rewrite ltn_double. apply toNatBounded. 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)