proposition: Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I -> C) : (forall i, P i -> `|F i| <= G i) -> \sum_(i | P i) F i = \sum_(i | P i) G i -> forall i, P i -> F i = G i.
proof: Proof. set sumF := \sum_(i | _) _; set sumG := \sum_(i | _) _ => leFG eq_sumFG. have posG i: P i -> 0 <= G i by move/leFG; apply: le_trans. have norm_sumG: `|sumG| = sumG by rewrite ger0_norm ?sumr_ge0. have norm_sumF: `|sumF| = \sum_(i | P i) `|F i|. apply/eqP; rewrite eq_le ler_norm_sum eq_sumFG norm_sumG -subr_ge0 -sumrB. by rewrite sumr_ge0 // => i Pi; rewrite subr_ge0 ?leFG. have [t _ defF] := normC_sum_eq norm_sumF. have [/(psumr_eq0P posG) G0 i Pi | nz_sumG] := eqVneq sumG 0. by apply/eqP; rewrite G0 // -normr_eq0 eq_le normr_ge0 -(G0 i Pi) leFG. have t1: t = 1. apply: (mulfI nz_sumG); rewrite mulr1 -{1}norm_sumG -eq_sumFG norm_sumF. by rewrite mulr_suml -(eq_bigr _ defF). have /psumr_eq0P eqFG i: P i -> 0 <= G i - F i. by move=> Pi; rewrite subr_ge0 defF // t1 mulr1 leFG. move=> i /eqFG/(canRL (subrK _))->; rewrite ?add0r //. by rewrite sumrB -/sumF eq_sumFG subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)