proposition: Lemma Log_lt_inv n x y : 1 < n -> 0 < x -> 0 < y -> Log n x < Log n y -> x < y.
proof: Proof. move=> n1 Hx Hy. rewrite /Log /Rdiv. have H : 0 < / ln n by exact/invR_gt0/ln_pos. move/(ltR_pmul2r H); exact: ln_lt_inv. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext