proposition: Lemma fft1E n (w : R) p : (2 ^ n).-primitive_root w -> fft1 n w p = fft n w p.
proof: Proof. elim: n w p => [// |n IH w p wE /=]. have wwE := prim_sqr wE. rewrite poly_def -(@big_mkord _ (0 : {poly R}) +%R (2 ^ n.+1) xpredT (fun (i : nat) => ((fft n (w ^+ 2) (even_poly p))`_(i %% 2 ^ n) + (fft n (w ^+ 2) (odd_poly p))`_(i %% 2 ^ n) * w ^+ i) *: 'X^i)). have F : (2 ^ n <= 2 ^ n.+1)%N by rewrite leq_exp2l. apply: sym_equal. rewrite (big_cat_nat _ _ _ _ F) //=. rewrite big_nat; under eq_bigr do rewrite modn_small // ; rewrite -big_nat /=. rewrite -(add0n (2 ^ n)%N) big_addn add0n. rewrite [(2 ^ n.+1)%N]expnS mul2n -addnn addnK. rewrite big_split /= big_mkord; congr (_ + _). by apply: eq_bigr => i _; rewrite !IH ?size_even_poly_exp2n ?size_odd_poly_exp2n //. rewrite big_nat; under eq_bigr do rewrite modnDr modn_small // exprD (prim_exp2nS wE) mulrN1 mulrN; rewrite -big_nat /=. rewrite big_mkord; apply: eq_bigr => i _. by rewrite !IH ?size_even_poly_exp2n ?size_odd_poly_exp2n. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn