proposition: Lemma all_results_fft1_reverse_poly p n w : (size p <= 2 ^ n)%N -> all_results_fft1 n 0 w p (reverse_poly n p).
proof: Proof. elim: n p => /= [p spL1|n IH p spLb]. by rewrite reverse_poly0 -poly_size1. split. rewrite /take_poly reverse_polyS poly_def. under eq_bigr do rewrite coefD coefMXn ifT // addr0. rewrite -poly_def. have -> : \poly_(i < 2 ^ n) (reverse_poly n (even_poly p))`_i = \poly_(i < size (reverse_poly n (even_poly p))) (reverse_poly n (even_poly p))`_i. apply/polyP => i; rewrite coef_poly [RHS]coef_poly. case: leqP => [n2Li|iLn2]. by rewrite ifN // -leqNgt (leq_trans _ n2Li) // size_reverse_poly. case: leqP => [epLi|iLep] => //. by suff /leq_sizeP-> : (size (reverse_poly n (even_poly p)) <= i)%N by []. rewrite coefK. apply: IH. by rewrite size_even_poly_exp2n. rewrite add0n. have -> : drop_poly (2 ^ n) (reverse_poly n.+1 p) = \poly_(i < 2 ^ n) (reverse_poly n.+1 p)`_(i + 2 ^ n). apply/polyP=> i; rewrite !coef_drop_poly !coef_poly. rewrite expnS mul2n -addnn ltn_add2r. by case: leqP => // nLn; rewrite nth_default. rewrite reverse_polyS poly_def. under eq_bigr do rewrite coefD coefMXn ltnNge leq_addl /= addnK scalerDl. rewrite big_split /= big1 ?add0r => [|i _]; last first. suff /leq_sizeP-> : (size (reverse_poly n (even_poly p)) <= i + 2 ^ n)%N. - by rewrite scale0r. - by []. by apply: leq_trans (size_reverse_poly _ _) (leq_addl _ _). rewrite -poly_def. have -> : \poly_(i < 2 ^ n) (reverse_poly n (odd_poly p))`_i = \poly_(i < size (reverse_poly n (odd_poly p))) (reverse_poly n (odd_poly p))`_i. apply/polyP => i; rewrite coef_poly [RHS]coef_poly. case: leqP => [n2Li|iLn2]. by rewrite ifN // -leqNgt (leq_trans _ n2Li) // size_reverse_poly. case: leqP => [epLi|iLep] => //. by suff /leq_sizeP-> : (size (reverse_poly n (odd_poly p)) <= i)%N by []. rewrite coefK. apply: IH. by rewrite size_odd_poly_exp2n. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn