proposition: Lemma istep_fft1 n p w : (size p <= 2 ^ n)%N -> istep n w p = fft1 n w p.
proof: Proof. move=> Hs. suff /(_ n 0%N): forall m1 n1 (p1 q1 : {poly R}), (size p1 <= 2 ^ (m1 + n1))%N -> (size q1 <= 2 ^ (m1 + n1))%N -> all_results_fft1 m1 n1 (w ^+ (2 ^ m1)) p1 q1 -> all_results_fft1 0 (m1 + n1) w p1 (istep_aux m1 n1 w q1). rewrite addn0 /=. apply => //; first by apply: size_reverse_poly. by apply: all_results_fft1_reverse_poly. elim => [//| m1 IH] n1 p1 q1 Hs1 Hs2 H1. rewrite /istep_aux -/istep_aux addSnnS. apply: IH; first by rewrite addnS. rewrite addnS. by apply: size_step. apply: all_results_fft1_step => //. by rewrite -exprM mulnC -expnS. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn