proposition: Lemma Variation_2 : forall x y, 1 < x -> x < y -> f x > f y.
proof: Proof. move => x y H1x Hxy. apply Ropp_lt_cancel. apply (incr_function (fun x => - f x) 1 p_infty (fun z => - ((2 - 2 - 2 * ln z) / z ^ 2))). move => z H1z _. apply: is_derive_opp. apply (Dfab 2 2 z). by apply Rlt_trans with (1 := Rlt_0_1). move => z H1z _. apply Ropp_lt_cancel ; rewrite Ropp_0 Ropp_involutive. apply sign_lt_0. rewrite -(is_derive_unique _ _ _ (Dfab 2 2 z (Rlt_trans _ _ _ Rlt_0_1 H1z))). rewrite Signe_df. apply -> sign_lt_0. apply Ropp_lt_cancel ; rewrite Ropp_0 Ropp_involutive. rewrite -ln_1. apply ln_increasing. by apply Rlt_0_1. by apply H1z. by apply Rlt_trans with (1 := Rlt_0_1). by []. by []. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)