proposition: Lemma invxln_prog_correct : forall beta p c x, nth 0 (Prog.eval_real (invxln_prog beta p) (x :: c)) 0 = (nth 0 (Prog.eval_real p (x :: c)) 0 / (x * pow (ln x) (S (S beta)))).
proof: Proof. intros beta p c x. unfold Prog.eval_real, invxln_prog. rewrite 2!Prog.rev_formula. rewrite rev_app_distr. simpl. replace (nth (length p) _ _) with x. now rewrite Pos2Nat.inj_succ, SuccNat2Pos.id_succ. 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