proposition: Lemma ltR_sumR_support (X : {set A}) : (0 < #|X|)%nat -> (forall i, i \in X -> f i < g i) -> \sum_(i in X) f i < \sum_(i in X) g i.
proof: Proof. move Hn : #|X| => n; elim: n X Hn => // n IH X Hn _ H. move: (ltn0Sn n); rewrite -Hn card_gt0; case/set0Pn => a0 Ha0. rewrite (@big_setD1 _ _ _ _ a0 _ f) //= (@big_setD1 _ _ _ _ a0 _ g) //=. case: n => [|n] in IH Hn. rewrite (_ : X :\ a0 = set0); first by rewrite !big_set0 2!addR0; exact: H. move: Hn. by rewrite (cardsD1 a0) Ha0 /= add1n => -[] /eqP; rewrite cards_eq0 => /eqP. apply ltR_add; first exact/H. apply IH => //. - by move: Hn; rewrite (cardsD1 a0) Ha0 /= add1n => -[]. - by move=> a; rewrite in_setD inE => /andP[_ ?]; exact: H. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)