proposition: Lemma is_derive_f_neg : forall beta x, beta <> 0%N -> 0 < x -> x <> 1 -> is_derive (fun x : R => f_neg x beta) x (/ (x * (ln x)^beta.+1)).
proof: Proof. intros beta x Hbeta Hx1 Hx2. rewrite /f_neg -[/(_ * _)]Ropp_involutive. apply: is_derive_opp. assert (H: (ln x <> 0)%R). rewrite <- ln_1. contradict Hx2. exact (ln_inv x 1 Hx1 Rlt_0_1 Hx2). auto_derive. - refine (conj Hx1 (conj _ I)). apply Rmult_integral_contrapositive. split. now apply not_0_INR. now apply pow_nonzero. - destruct beta as [|beta]. easy. simpl Nat.pred. simpl pow. field. repeat split. now apply pow_nonzero. exact H. now apply Rgt_not_eq. now apply not_0_INR. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval