proposition: Lemma epsilon_trick0 (R : realType) (eps : R) (P : pred nat) : (0 <= eps)%R -> \sum_(i <oo | P i) (eps / (2 ^ i.+1)%:R)%:E <= eps%:E.
proof: Proof. move=> epspos; have := epsilon_trick P (fun=> lexx 0) epspos. rewrite (@eq_eseriesr _ (fun n => 0 + _) (fun n => (eps/(2^n.+1)%:R)%:E)). by move/le_trans; apply; rewrite eseries0 ?add0e; [exact: lexx | move=> ? ?]. by move=> ? ?; rewrite add0e. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)