proposition: Lemma toNatBounded n : forall (p: BITS n), toNat p < 2^n.
proof: Proof. induction n. move => p. by rewrite toNatNil. case/tupleP => [b p]. rewrite expnS mul2n toNatCons. case b. + rewrite ltn_Sdouble. apply IHn. + rewrite ltn_double. apply IHn. 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