proposition: Lemma contains_RInt_gen_zero_bertrand_pow0 : forall prec deg limit check vars hyps beta pf pv cf cv, R.eval_hyps_bnd (R.merge_hyps prec hyps) vars -> no_floor_prog pf = true -> let hyps := R.merge_hyps prec hyps in let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps (bertrand_zero_interval 0 beta) pf (bertrand_prog 0 beta pf) pv cf cf cv in contains (I.convert (IR.bisect prec limit mid Fi check)) (Xreal (RInt_gen (fun t => Prog.eval_real' pf (t :: vars) cf * pow (ln t) beta) (at_right 0) (at_point (Prog.eval_real' pv vars cv)))).
proof: Proof. intros prec deg limit check vars hyps beta pf pv cf cv H' Hp. generalize (contains_RInt_gen_zero_bertrand prec deg limit check vars hyps 0 beta pf pv cf cv H' eq_refl Hp). cbv zeta. intro H. rewrite RInt_gen_ext_eq with (g := (fun t : R => eval_real' pf (t :: vars) cf * (powerRZ t 0 * ln t ^ beta))). exact H. intros x. now rewrite powerRZ_O, Rmult_1_l. 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