proposition: Lemma leR_sumR_eq (A : finType) (f g : A -> R) (P : pred A) : (forall a, P a -> f a <= g a) -> \sum_(a | P a) g a = \sum_(a | P a) f a -> (forall a, P a -> g a = f a).
proof: Proof. move=> H1 H2 i Hi; rewrite -subR_eq0; move: i Hi; apply: psumr_eq0P. by move=> i Pi; rewrite RminusE subr_ge0; apply/RleP/H1. by rewrite big_split/= -big_morph_oppR; apply/eqP; rewrite subr_eq0 H2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)