proposition: Lemma leR_sumRl_support (U : pred A) : (forall a, 0 <= f a) -> (forall i, P i -> Q i) -> \sum_(i in U | P i) f i <= \sum_(i in U | Q i) f i.
proof: Proof. move=> Hf P_Q; elim: (index_enum _) => [|h t IH]. - by rewrite !big_nil; apply/RleP; rewrite lexx. - rewrite !big_cons; case: (h \in U) => //=; case: ifP => // Ph. + by case: ifP => [Qh|]; [rewrite leR_add2l | rewrite (P_Q _ Ph)]. + by case: ifP => // Qh; rewrite -[X in X <= _]add0R; exact/leR_add. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)