proposition: Lemma sumrB I r (P : pred I) (F1 F2 : I -> V) : \sum_(i <- r | P i) (F1 i - F2 i) = \sum_(i <- r | P i) F1 i - \sum_(i <- r | P i) F2 i.
proof: Proof. by rewrite -sumrN -big_split /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)