proposition: Lemma psum_exists {R : realType} {A : choiceType} {f : A -> R} (H : 0 < realsum.psum (T:=A) (R:=R) f) (Hpos : forall x, 0 <= f x) : exists x, 0 < f x.
proof: Proof. assert (realsum.psum f ≠ 0) as Hneq. { intros Hgt. rewrite Hgt in H. rewrite order.Order.POrderTheory.ltxx in H. auto. } destruct (realsum.neq0_psum (R:=R) Hneq) as [x Hx]. exists x. specialize (Hpos x). rewrite order.Order.POrderTheory.le_eqVlt in Hpos. move: Hpos. move /orP => [H1 | H2]. - move: H1. move /eqP => H1. rewrite -H1. rewrite order.Order.POrderTheory.ltxx. auto. - assumption. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)