proposition: Lemma toNat_shrB n : forall (p: BITS n), toNat (shrB p) = (toNat p)./2.
proof: Proof. destruct n. move => p. by rewrite (tuple0 p). case/tupleP => [b p]. by rewrite /shrB toNat_joinmsb0 /droplsb/splitlsb beheadCons theadCons toNatCons half_bit_double. 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)