proposition: Theorem eval_RInt_gen_infty_bertrand : forall prec deg limit vars hyps alpha beta pg pf pu cg cf cu g, (alpha < -1)%Z -> no_floor_prog pf = true -> eval_RInt_gen_infty prec deg limit hyps (bertrand_infty_interval alpha beta) pg pf (bertrand_prog alpha beta pf) pu cg cf cf cu g = true -> eval_hyps hyps vars ( eval_goal g (Prog.eval_real' pg ( (RInt_gen (fun t => Prog.eval_real' pf (t :: vars) cf * (powerRZ t alpha * pow (ln t) beta)) (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)) :: vars) cg)).
proof: Proof. intros prec deg limit vars hyps alpha beta pg pf pu cg cf cu g Halpha Hp H. apply (R.eval_hyps_bnd_correct prec). intros H'. apply (R.eval_goal_bnd_correct prec) with (2 := H). unfold eval_real'. simpl. fold (compute_inputs prec hyps cg). apply A.BndValuator.eval_correct_ext'. now apply app_merge_hyps_eval_bnd. now apply contains_RInt_gen_infty_bertrand. 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