proposition: Lemma all_resultsS_fft1 n m w p q : all_results_fft1 n.+1 m w p q <-> all_results_fft1 n m w (even_poly p) (take_poly (2 ^ (m + n)) q) /\ all_results_fft1 n m w (odd_poly p) (drop_poly (2 ^ (m + n)) q).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn