proposition: Lemma fromNat_wrap n : forall m, fromNat (n:=n) m = fromNat (n:=n) (m + 2^n).
proof: Proof. induction n => //. rewrite expnS. move => m. case ODD: (odd m); rewrite /fromNat-/fromNat /=ODD oddD oddM/=ODD/= halfD ODD/=. specialize (IHn m./2). by rewrite oddM/= add0n mul2n doubleK IHn. specialize (IHn m./2). by rewrite add0n mul2n doubleK 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