proposition: Lemma all_results_fft1_step m n w (p q : {poly R}): (size p <= 2 ^ (m + n).+1)%N -> (size q <= 2 ^ (m + n).+1)%N -> all_results_fft1 m.+1 n (w ^+ 2) p q -> all_results_fft1 m n.+1 w p (step m n w q).
proof: Proof. elim: m n w p q => [n p w q| m IH n w p q Hsp Hsp1/all_resultsS_fft1[H2 H3]]. rewrite add0n => Hp Hq [H1 H2]. rewrite /= -H1 -H2 /step big_ord1 mul0n !addn0. apply: eq_bigr => /= i _. by rewrite !coef_drop_poly !coef_poly !addn0 ltn_ord. apply/all_resultsS_fft1; split. rewrite [(_ + m)%N]addnC addnS take_step //. apply: IH => //. - by apply: size_even_poly_exp2n. - by rewrite size_poly. by rewrite [(m + _)%N]addnC -addnS. rewrite addnC addnS drop_step //. apply: IH => //. - by apply: size_odd_poly_exp2n. - rewrite size_drop_poly. by rewrite leq_subLR addnn -mul2n -expnS. by rewrite [(m + _)%N]addnC -addnS. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn