proposition: Lemma Log_increasing_le n x y : 1 < n -> 0 < x -> x <= y -> Log n x <= Log n y.
proof: Proof. move=> n1 x0 xy. apply leR_wpmul2r. apply/RleP. rewrite RinvE//; last first. rewrite gtR_eqF//. exact/ln_pos. by rewrite invr_ge0; exact/ltW/RltP/ln_pos. exact: ln_increasing_le. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext