proposition: Lemma toNat_mod n (p:BITS n): toNat p = toNat p %% 2^n.
proof: Proof. rewrite modn_small => //. apply toNatBounded. 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