proposition: Lemma toNat_fromNat n m : @toNat n (fromNat m) = m %% 2^n.
proof: Proof. have H:= divn_eq m (2^n). rewrite {1}H. have HH:= @fromNat_wrapMany n (m %/ 2^n) (m %% 2^n). rewrite addnC in HH. rewrite -HH. rewrite toNat_fromNatBounded. done. apply ltn_pmod. apply expn_gt0. 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