proposition: Lemma leR_sumRl : (forall i, P i -> f i <= g i) -> (forall i, Q i -> 0 <= g i) -> (forall i, P i -> Q i) -> \sum_(i | P i) f i <= \sum_(i | Q i) g i.
proof: Proof. move=> f_g Qg H; elim: (index_enum _) => [| h t IH]. - rewrite !big_nil. by apply/RleP; rewrite lexx. - rewrite !big_cons /=; case: ifP => [Ph|Ph]. by rewrite (H _ Ph); apply leR_add => //; exact: f_g. case: ifP => // Qh; apply: (leR_trans IH). by rewrite -{1}[X in X <= _](add0R _); exact/leR_add2r/Qg. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)