proposition: Lemma Variation_1 : forall x y, 0 < x -> x < y -> y < 1 -> f x < f y.
proof: Proof. apply (incr_function _ 0 1 (fun x => (2 - 2 - 2 * ln x) / x ^ 2)). move => x H0x Hx1. by apply (Dfab 2 2 x). move => x H0x Hx1. apply sign_0_lt. rewrite -(is_derive_unique _ _ _ (Dfab 2 2 x H0x)). rewrite Signe_df. apply -> sign_0_lt. apply Ropp_lt_cancel ; rewrite Ropp_0 Ropp_involutive. rewrite -ln_1. by apply ln_increasing. by apply H0x. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)