proposition: Lemma left_step m n (p : {poly R}) : (size p <= 2 ^ (m + n).+2)%N -> left_poly (2 ^ (m + n).+1) (step m.+1 n p) = step m n (left_poly (2 ^ (m + n).+1) p).
proof: Proof. move=> pLmn. apply/polyP=> i; rewrite coef_left_poly. case: leqP => [mnLi|iLmn]. rewrite nth_default //. by apply: leq_trans (size_step _ _ _) _. rewrite !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 ((merge _ _ _ * _) `_ _). apply/polyP => k; rewrite !coef_poly. case: leqP => // kLn. rewrite ifT // -[in X in (_ < X)%N]addnS expnD. rewrite -[X in (_ < X * _)%N]prednK ?expn_gt0 // mulSn -addSn. apply: leq_add. by apply: leq_trans kLn _; rewrite leq_exp2l. by rewrite leq_mul2r -ltnS prednK ?expn_gt0 // ltn_ord orbT. apply/polyP => k; rewrite !coef_poly. case: leqP => // kLn. rewrite ifT // -[in X in (_ < X)%N]addnS expnD addnAC. rewrite -[X in (_ < X * _)%N]prednK ?expn_gt0 // mulSn -addSn. apply: leq_add. by rewrite expnS mul2n -addnn ltn_add2r. by rewrite leq_mul2r -ltnS prednK ?expn_gt0 // ltn_ord orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)