proposition: Lemma LogK n x : 1 < n -> 0 < x -> Exp n (Log n x) = x.
proof: Proof. move=> n1 x0. rewrite /Log /Exp -mulRA mulVR ?mulR1 ?exp_ln //. 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