proposition: Lemma LogV n x : 0 < x -> Log n (/ x) = - Log n x.
proof: Proof. by move=> x0; rewrite /Log ln_Rinv // -mulNR. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext