proposition: Lemma rmodp_sum (I : Type) (r : seq I) (P : pred I) (F : I -> {poly R}) : rmodp (\sum_(i <- r | P i) F i) d = (\sum_(i <- r | P i) (rmodp (F i) d)).
proof: Proof. by elim/big_rec2: _ => [|i p q _ <-]; rewrite ?(rmod0p, rmodpD). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)