proposition: Lemma seq_psume_eq0 (I : choiceType) (r : seq I) (P : pred I) (F : I -> \bar R) : (forall i, P i -> 0 <= F i)%E -> (\sum_(i <- r | P i) F i == 0)%E = all (fun i => P i ==> (F i == 0%E)) r.
proof: Proof. move=> F0; apply/eqP/allP => PF0; last first. rewrite big_seq_cond big1// => i /andP[ir Pi]. by have := PF0 _ ir; rewrite Pi implyTb => /eqP. move=> i ir; apply/implyP => Pi; apply/eqP. have rPF : {in r, forall i, P i ==> (F i \is a fin_num)}. move=> j jr; apply/implyP => Pj; rewrite fin_numElt; apply/andP; split. by rewrite (lt_le_trans _ (F0 _ Pj))// ltNyr. rewrite ltNge; apply/eqP; rewrite leye_eq; apply/eqP/negP => /eqP Fjoo. have PFninfty k : P k -> F k != -oo%E. by move=> Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNyr. have /esum_eqyP : exists i, [/\ i \in r, P i & F i = +oo%E] by exists j. by move=> /(_ PFninfty); rewrite PF0. have ? : (\sum_(i <- r | P i) (fine \o F) i == 0)%R. apply/eqP/EFin_inj; rewrite big_seq_cond -sumEFin. rewrite (eq_bigr (fun i0 => F i0)); last first. move=> j /andP[jr Pj] /=; rewrite fineK//. by have := rPF _ jr; rewrite Pj implyTb. by rewrite -big_seq_cond PF0. have /allP/(_ _ ir) : all (fun i => P i ==> ((fine \o F) i == 0))%R r. by rewrite -psumr_eq0// => j Pj/=; apply/fine_ge0/F0. rewrite Pi implyTb => /= => /eqP Fi0. rewrite -(@fineK _ (F i))//; last by have := rPF _ ir; rewrite Pi implyTb. by rewrite Fi0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed