proposition: Lemma ExpK n x : 1 < n -> Log n (Exp n x) = x.
proof: Proof. move=> n1. rewrite /Log /Exp ln_exp /Rdiv -mulRA mulRV ?mulR1 //. rewrite -ln_1; apply/eqP => /ln_inv H. have : 0 < n by lra. move/H => /(_ Rlt_0_1) ?; lra. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext