proposition: Lemma Signe_df : forall x, 0 < x -> sign (Derive f x) = sign (- ln x).
proof: Proof. move => x Hx. rewrite (is_derive_unique f x _ (Dfab 2 2 x Hx)). replace ((2 - 2 - 2 * ln x) / x ^ 2) with (2 / x ^ 2 * (- ln x)) by (field ; now apply Rgt_not_eq). rewrite sign_mult sign_eq_1. apply Rmult_1_l. apply Rdiv_lt_0_compat. apply Rlt_0_2. apply pow2_gt_0. by apply Rgt_not_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)