proposition: Lemma ltR_sumR : (O < #|A|)%nat -> (forall i, f i < g i) -> \sum_(i in A) f i < \sum_(i in A) g i.
proof: Proof. move=> A0 H0. have : forall i : A, i \in [set: A] -> f i < g i by move=> a _; exact/H0. move/ltR_sumR_support; rewrite cardsT => /(_ A0). rewrite big_mkcond /= [in X in _ < X]big_mkcond /=. rewrite (eq_bigr f) //; last by move=> *; rewrite inE. by rewrite [in X in _ < X](eq_bigr g) // => *; rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)