proposition: Lemma invariant_algo_step m n p p1 : (size p <= 2 ^ (m + n).+1)%N -> (size p1 <= 2 ^ (m + n).+1)%N -> invariant_algo m.+1 n p p1 -> invariant_algo m n.+1 p (step m n p1).
proof: Proof. elim: m n p p1; last first. move=> m IH n p p1 Hsp Hsp1/invariantS_algo[H2 H3]. apply/invariantS_algo; split. rewrite addnS left_step //. apply: IH => //. by apply: leq_trans (size_left _) _. by rewrite size_poly. rewrite addnS right_step //. apply: IH => //. by apply: leq_trans (size_right _) _. by rewrite size_poly. move=> n p p1; rewrite add0n => Hp Hp1 [H1 H2]. rewrite /= -H1 -H2. rewrite /step big_ord1 mul0n mulr1. by congr (merge _ _ _); apply/polyP=> i; rewrite !coef_poly !add0n !addn0. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)