proposition: Lemma logDiv x y : 0 < x -> 0 < y -> log (x / y) = log x - log y.
proof: Proof. move=> x0 y0; exact: (@LogDiv 2 _ _ x0 y0). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext