proposition: Lemma stepE m n w (p : {poly R}) : step m n w p = \sum_(l < 2 ^ m) let ev := \poly_(i < 2 ^ n) p`_(i + l * 2 ^ n.+1) in let ov := \poly_(i < 2 ^ n) p`_(i + l * 2 ^ n.+1 + 2 ^ n) in (\sum_(j < 2 ^ n) ((ev`_j + ov`_ j * w ^+ j) *: 'X^j + (ev`_j - ov`_ j * w ^+ j) *: 'X^(j + 2 ^ n))) * 'X^ (l * 2 ^ n.+1).
proof: Proof. apply: eq_bigr => i _ /=. rewrite [RHS]mulr_suml. apply: eq_bigr => j _ /=. rewrite mulrDl; congr (_ + _); rewrite -scalerAl -exprD //. by rewrite addnAC. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn