proposition: Lemma right_step m n (p : {poly R}) : (size p <= 2 ^ (m + n).+2)%N -> right_poly (2 ^ (m + n).+1) (step m.+1 n p) = step m n (right_poly (2 ^ (m + n).+1) p).
proof: Proof. move=> pLmn. apply/polyP=> i; rewrite coef_right_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 ?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 // (leq_trans (size_merge _ _)) // ?size_poly //. 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 ((merge _ _ _) `_ _). apply/polyP => k; rewrite !coef_poly. case: leqP => // kLn. rewrite ifT; first by rewrite addnAC addnA. rewrite -[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. rewrite -!addnA. congr (_ `_ (_ + _)); first by rewrite addnC !addnA. rewrite addnAC -[in X in (_ < X)%N]addnS expnD. 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)