fact: Fixpoint fft (n : nat) (w : R) (p : {poly R}) : {poly R} := if n is n1.+1 then let ev := fft n1 (w ^+ 2) (even_poly p) in let ov := fft n1 (w ^+ 2) (odd_poly p) in \poly_(i < 2 ^ n1.+1) let j := (i %% 2 ^ n1)%N in ev`_j + ov`_ j * w ^+ i else (p`_0)%:P.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn