proposition: Lemma take_step m n w (p : {poly R}) : (size p <= 2 ^ (m + n).+2)%N -> take_poly (2 ^ (m + n).+1) (step m.+1 n w p) = step m n w (take_poly (2 ^ (m + n).+1) p).
proof: Proof. move=> pLmn; rewrite stepE. apply/polyP=> i; rewrite coef_take_poly. case: leqP => [mnLi|iLmn]. rewrite nth_default //. by apply: leq_trans (size_step _ _ _ _) _. rewrite stepE !coef_sum expnS mul2n -addnn big_split_ord /=. rewrite [X in _ + X = _]big1 ?addr0 => [|j _]; last first. by rewrite coefMXn ifT // (leq_trans iLmn) // mulnDl -expnD addnS leq_addr. apply: eq_bigr => j _. congr (((_ * _) : {poly R}) `_ _). apply: eq_bigr => k _. have F : (k + j * 2 ^ n.+1 < 2 ^ (m + n).+1)%N. apply: leq_trans (bound_step (ltn_ord j) (ltn_ord k)). by rewrite ltnS leq_addr. have F1 : (k + j * 2 ^ n.+1 + 2 ^ n < 2 ^ (m + n).+1)%N. by apply: bound_step. by rewrite !coef_poly F F1. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn