proposition: Lemma invariant_algo_bottom p m : invariant_algo m 0 p (bottom m p).
proof: Proof. elim: m p => //= m IH p. rewrite addn0 left_poly_add right_poly_add; split. rewrite left_polyMXn addr0 left_poly_id; first by by apply: IH. by apply: size_bottom. rewrite (right_poly_size_0 (size_bottom _ _)) add0r. rewrite right_polyMXn; last by apply: size_bottom. by apply: IH. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)