proposition: Lemma right_polyMXn m p : (size p <= m)%N -> right_poly m ('X^ m * p) = p.
proof: Proof. move=> Hs; apply/polyP => i. rewrite -[_ * p]commr_polyXn coef_poly coefMXn addnK. rewrite [(_ + _ < _)%N]ltnNge leq_addl /=. case: leqP => // mLi. by apply/sym_equal/nth_default/(leq_trans _ mLi). Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)