proposition: Lemma fftE n (w : R) p : (size p <= 2 ^ n)%N -> (2 ^ n).-primitive_root w -> fft n w p = \poly_(i < 2 ^ n) p.[w ^+ i].
proof: Proof. elim: n w p => [/= w p sL _ |n IH w p sL wE /=]. by rewrite poly_def big_ord1 expr0 [p]poly_size1 // !hornerE alg_polyC coefC. apply/polyP => i; rewrite !coef_poly; case: leqP => // iL. have imL : (i %% 2 ^ n < 2 ^ n)%N by apply/ltn_pmod/expn_gt0. have n2P : (0 < 2 ^ n.+1)%N by rewrite expn_gt0. have wwE := prim_sqr wE. rewrite !IH ?coef_poly ?imL ?size_even_poly_exp2n ?size_odd_poly_exp2n //. rewrite -[p in RHS]poly_even_odd. rewrite !(hornerD, horner_comp, hornerMX, hornerX). suff -> : (w ^+ 2) ^+ (i %% 2 ^ n) = w ^+ i * w ^+ i by []. rewrite -!expr2 -!exprM. have [iLm|mLi] := leqP (2 ^ n) i; last by rewrite modn_small // mulnC. have -> : (i %% 2 ^ n = i - 2 ^ n)%N. rewrite -[in LHS](subnK iLm) modnDr modn_small //. by rewrite ltn_psubLR ?expn_gt0 // addnn -mul2n -expnS. have -> : (i * 2 = 2 * (i - 2 ^ n) + 2 ^ n.+1)%N. by rewrite mulnC mulnBr -expnS subnK // expnS leq_mul2l. rewrite exprD. suff -> : w ^+ (2 ^ n.+1) = 1 by rewrite mulr1. by rewrite expnS exprM (prim_expr_order wwE). Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn