proposition: Corollary toNat_dropmsb n (p: BITS n.+1) : toNat (dropmsb p) = toNat p %% 2^n.
proof: Proof. rewrite -{1}(toNatK p). rewrite dropmsb_fromNat. by rewrite toNat_fromNat. 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