proposition: Lemma f_correct alpha beta A B (H : 0 < A <= B) (Halpha: alpha <> (-1)%Z) : Bertrand alpha beta A B (f alpha beta A B).
proof: Proof. elim: beta => [|m HIm] // . rewrite /f /Bertrand. apply: (is_RInt_ext (fun x => powerRZ x alpha)). + by move => x Hx; rewrite pow_O Rmult_1_r. exact: int_x_alpha. by move: (one_step_by_parts alpha m A B H Halpha _ HIm). Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval