proposition: Lemma right_poly_sum m n (p : 'I_n -> {poly R}) : right_poly m (\sum_(i < n) p i) = \sum_(i < n) (right_poly m (p i)).
proof: Proof. have F (q : nat -> _) : right_poly m (\sum_(i < n) q i) = \sum_(i < n) (right_poly m (q i)). elim: n {p}q => [|n IH] q; first by rewrite !big_ord0 right_poly0. by rewrite !big_ord_recr /= right_poly_add IH. case: n p F => [|n] p F; first by rewrite !big_ord0 right_poly0. have := F (fun x => p (inord x)). under eq_bigr do rewrite inord_val. by under [X in _ = X -> _]eq_bigr do rewrite inord_val. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum)