proposition: Lemma ln_div x y : 0 < x -> 0 < y -> ln (x / y) = ln x - ln y.
proof: Proof. intros Hx Hy ; unfold Rdiv. rewrite ln_mult. rewrite ln_Rinv. ring. exact Hy. exact Hx. apply Rinv_0_lt_compat ; exact Hy. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)