proposition: Lemma right_poly_add m (p q : {poly R}) : right_poly m (p + q) = right_poly m p + right_poly m q.
proof: Proof. apply/polyP => i; rewrite !(coefD, coef_poly). by case: leqP; rewrite ?add0r. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)