proposition: Lemma toNat_rolB n (p: BITS n.+1) : toNat (rolB p) = (toNat p %% 2^n).*2 + toNat p %/ 2^n.
proof: Proof. rewrite /rolB. rewrite -(toNatK p) splitmsb_fromNat (toNatK p). rewrite toNatCons toNat_fromNat. rewrite addnC. have H:= toNatBounded p. case E: (toNat p %/ 2^n) => [| n']. + by rewrite addn0. + case E': n' => [| n'']. done. + rewrite E' in E. rewrite expnS in H. rewrite -ltn_divLR in H; last apply expn_gt0. rewrite E in H. subst. destruct n'' => //. 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)