proposition: Lemma fftK n (w : F) p : 2%:R != 0 :> F -> (size p <= 2 ^ n)%N -> (2 ^ n).-primitive_root w -> ifft n w (fft n w p) = p.
proof: Proof. move=> char2 sL wE. have wE1 : w ^+ (2 ^ n) = 1 by apply: prim_expr_order. have wNZ : w != 0. apply/eqP=> wZ; move/eqP: wE1. by rewrite eq_sym wZ expr0n expn_eq0 /= oner_eq0. have wVE := primJ wE. have wIE : w^-1 = w ^+ (2 ^ n).-1. by apply: (mulfI wNZ); rewrite mulfV // -exprS prednK ?expn_gt0. rewrite /ifft !fftE ?size_poly //. apply/polyP => i; rewrite coefCM coef_poly /=. case: leqP => iL; first by rewrite nth_default ?mulr0 // (leq_trans _ iL). rewrite horner_poly. have pE : p = \poly_(j < 2 ^ n) p`_j. apply/polyP => j; rewrite coef_poly; case: leqP => // jL. by rewrite nth_default // (leq_trans _ jL). under [X in _ * X = _]eq_bigr => j H do rewrite {1}pE horner_poly /= mulr_suml (bigD1 (Ordinal iL)) //= -!exprM mulnC -mulrA -exprMn ?(divff, expr1n, mulr1, addr0) //. rewrite big_split /=. rewrite sumr_const card_ord mulrDr. rewrite -[X in _ * X + _ = _]mulr_natl mulrA mulVf ?mul1r; last first. by rewrite natrX expf_eq0 (negPf char2) andbF. rewrite exchange_big /= big1 ?(mulr0, addr0) //= => k /eqP /val_eqP /= kDi. under [LHS] eq_bigr do rewrite -mulrA -exprM mulnC !exprM -exprMn wIE -!exprM -exprD. set x := w ^+ _; rewrite -mulr_sumr. suff xDone : x - 1 != 0. suff -> : (\sum_(i0 < 2 ^ n) x ^+ i0) = 0 by rewrite mulr0. apply: (mulfI xDone). by rewrite -subrX1 mulr0 -exprM mulnC exprM wE1 expr1n subrr. rewrite subr_eq0 -(prim_order_dvd wE). case: {x}i iL kDi => [|i] iL xDi. rewrite muln0 addn0; apply/negP=> /dvdn_leq. by rewrite lt0n leqNgt ltn_ord => /(_ xDi). rewrite -subn1 mulnBl mul1n mulnS addnC [(_ ^ _ + _)%N]addnC. rewrite -addnBA ?(leq_trans _ iL) //. rewrite /dvdn mulnC -addnA modnMDl; apply/negP => /dvdnP[q /eqP qE]. suff : (q < 2)%N. case: q qE => [|[|]] //. by rewrite mul0n; rewrite addn_eq0 subn_eq0 leqNgt iL. by rewrite mul1n -(eqn_add2r (i.+1)) addnAC subnK ?(eqn_add2l, negPf xDi) // ltnW. rewrite -(ltn_pmul2r (_ : 0 < 2 ^ n)%N) ?expn_gt0 //. rewrite -(eqP qE) mul2n -addnn. apply: (leq_trans (_ : _ <= 2 ^ n - i.+1 + 2 ^ n)%N). by rewrite ltn_add2l. by rewrite leq_add2r leq_subr. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn