proposition: Theorem eval_RInt_gen_infty_contains_invxln : forall prec deg limit vars hyps beta pf pu cf cu b, no_floor_prog pf = true -> eval_RInt_gen_infty_contains prec deg limit hyps (invxln_interval beta) pf (invxln_prog beta pf) pu cf cf cu b = true -> eval_hyps hyps vars ( contains (I.convert b) (Xreal (RInt_gen (fun t => Prog.eval_real' pf (t :: vars) cf / (t * pow (ln t) (S (S beta)))) (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)))).
proof: Proof. intros prec deg limit vars hyps beta pf pu cf cu b Hp H. apply (R.eval_hyps_bnd_correct prec). intros H'. apply I.subset_correct with (2 := H). now apply contains_RInt_gen_infty_invxln. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Coquelicot(Coquelicot) Stdlib Coquelicot Xreal Basic Sig Interval Integral Eval Bertrand Tree Prog Reify Refine Interval_helper