proposition: Lemma left_poly_add m (p q : {poly R}) : left_poly m (p + q) = left_poly m p + left_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)