proposition: Lemma toNat_fromNatBounded n : forall m, m < 2^n -> toNat (fromNat (n:=n) m) = m.
proof: Proof. induction n. + rewrite expn0. by case. + rewrite expnS. move => m. specialize (IHn m./2). move => LT. assert (m./2 < 2^n). rewrite -ltn_double. rewrite -(odd_double_half m) mul2n in LT. rewrite -(ltn_add2l (odd m)). by apply ltn_addl. specialize (IHn H). rewrite /toNat-/toNat/=. rewrite /toNat/= in IHn. rewrite IHn. by rewrite odd_double_half. 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