proposition: Lemma toNat_droplsb n (p: BITS n.+1) : toNat (droplsb p) = (toNat p)./2.
proof: Proof. case/tupleP: p => [b p]. rewrite /droplsb/splitlsb beheadCons theadCons. by rewrite toNatCons/= half_bit_double. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec