proposition: Lemma Log_n (n : R) : 1 < n -> Log n n = 1.
proof: Proof. by move=> n1; rewrite /Log /Rdiv mulRV //; exact/gtR_eqF/ln_pos. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext