fact: Fixpoint all_results_fft1 n m w p q := if n is n1.+1 then all_results_fft1 n1 m w (even_poly p) (take_poly (2 ^ (m + n1)) q) /\ all_results_fft1 n1 m w (odd_poly p) (drop_poly (2 ^ (m + n1)) q) else q = fft1 m w p.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn