proposition: Lemma toNat_rorB n (p: BITS n.+1) : toNat (rorB p) = (toNat p)./2 + (toNat p %% 2) * 2^n.
proof: Proof. case/tupleP: p => [b p]. rewrite /rorB toNat_joinmsb /droplsb/splitlsb beheadCons theadCons toNatCons /=. rewrite half_bit_double. rewrite modn2 oddD odd_double addnC. by destruct b. 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)