proposition: Lemma right_poly_size_0 m p : (size p <= m)%N -> right_poly m p = 0.
proof: Proof. move=> Hs; apply/polyP => i. rewrite coef_poly coef0; case: leqP => // Hs1. apply: nth_default. by apply: leq_trans Hs (leq_addl _ _). Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)