proposition: Lemma drop_step m n w (p : {poly R}) : (size p <= 2 ^ (m + n).+2)%N -> drop_poly (2 ^ (m + n).+1) (step m.+1 n w p) = step m n w (drop_poly (2 ^ (m + n).+1) p).
proof: Proof. move=> pLmn. apply/polyP=> i; rewrite coef_drop_poly. rewrite !stepE !coef_sum expnS mul2n -addnn big_split_ord /=. rewrite [X in X + _ = _]big1 ?add0r => [|j _]; last first. rewrite coefMXn ifN; last first. rewrite -leqNgt (leq_trans _ (leq_addl _ _)) //. by rewrite -addnS expnD leq_mul2r // ltnW ?orbT. rewrite nth_default //. apply: leq_trans (_ : 2 ^ n.+1 <= _)%N. apply: leq_trans (size_sum _ _ _) _. apply/bigmax_leqP => k _. apply: leq_trans (size_add _ _) _. rewrite geq_max; apply/andP; split; apply: leq_trans (size_scale_leq _ _) _. rewrite size_polyXn. by apply: leq_trans (ltn_ord _) _; rewrite leq_exp2l. by rewrite size_polyXn expnS mul2n -addnn ltn_add2r. rewrite leq_subRL (leq_trans _ (leq_addl _ _)) //. by rewrite addnC -mulSn -addnS expnD leq_mul2r ltn_ord orbT. by rewrite -addnS expnD leq_mul2r ltnW ?orbT // ltn_ord. apply: eq_bigr => j _. rewrite !coefMXn addnC mulnDl -expnD addnS ltn_add2l. case: leqP => // jLi; rewrite subnDl. congr ((_ : {poly R}) `_ _). apply: eq_bigr => k _. have F : (k + j * 2 ^ n.+1 + 2 ^ (m + n).+1 = k + (2 ^ (m + n).+1 + j * 2 ^ n.+1))%N. by rewrite addnAC addnA. have F1 : ((k + j * 2 ^ n.+1 + 2 ^ n + 2 ^ (m + n).+1) = (k + (2 ^ (m + n).+1 + j * 2 ^ n.+1) + 2 ^ n))%N. by rewrite !addnA [(k + _ + _)%N in RHS]addnAC [(_ + 2 ^ n)%N in RHS]addnAC. by rewrite !(coef_drop_poly, coef_poly) ltn_ord // F F1. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn