proposition: Lemma istep1_fft1 n p w : (size p <= 2 ^ n)%N -> istep1 n w p = fft1 n w p.
proof: Proof. move=> Hs; rewrite -istep_fft1 // /istep1 /istep. elim: n {Hs}(size_reverse_poly n p) 0%N w (reverse_poly _ _) => //= n IH pLn n1 w p1. rewrite step1E. apply: IH. by apply: size_reverse_poly. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn