proposition: Lemma leR_sumR_support (X : {set A}) : (forall i, i \in X -> P i -> f i <= g i) -> \sum_(i in X | P i) f i <= \sum_(i in X | P i) g i.
proof: Proof. move=> H; elim/big_rec2 : _ => //. exact: Rle_refl. move=> a x y /andP[aX Pa] yx. by apply leR_add => //; apply: H. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)