proposition: Lemma bertrand_prog_correct : forall alpha beta p c x, nth 0 (Prog.eval_real (bertrand_prog alpha beta p) (x :: c)) 0 = (nth 0 (Prog.eval_real p (x :: c)) 0 * (powerRZ x alpha * pow (ln x) beta)).
proof: Proof. intros alpha beta p c x. unfold Prog.eval_real, bertrand_prog. rewrite 2!Prog.rev_formula. rewrite rev_app_distr. simpl. replace (nth (length p) _ _) with x. now rewrite <- pow_powerRZ. rewrite <- rev_length. now induction (rev p) as [|h t]. 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