proposition: Lemma natsumrB A (P : A -> bool) F1 F2 l : (forall i, (P i -> F1 i >= F2 i)) -> \sum_(i <- l | P i) F1 i - \sum_(i <- l | P i) F2 i = \sum_(i <- l | P i) (F1 i - F2 i).
proof: Proof. move => Hge; elim: l => [|a l Hl]; first by rewrite !big_nil. rewrite !big_cons; case HPa: (P a); rewrite // subnDA -addnBAC ?Hge //. by rewrite -addnBA ?Hl // leq_sum. Qed.
imports: mathcomp(all_ssreflect all_algebra)