proposition: Lemma Log_increasing n a b : 1 < n -> 0 < a -> a < b -> Log n a < Log n b.
proof: Proof. move=> n1 Ha a_b. rewrite /Log; apply ltR_pmul2r; last exact: ln_increasing. exact/invR_gt0/ln_pos. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext