proposition: Lemma log_id_diff x y : 0 <= x -> (y = 0 -> x = 0) -> 0 <= y -> x * (log (y / x)) = (y - x) * log (exp 1) -> x = y.
proof: Proof. move=> Hx Hxy /leR_eqVlt[/esym|] y0 Hxy2; first by rewrite y0 Hxy. case/leR_eqVlt : Hx => [/esym|] x0. - move/esym : Hxy2; rewrite x0 mul0R subR0 mulR_eq0 => -[] //. by rewrite logexp1E => /invR_eq0/eqP; rewrite (negbTE ln2_neq0). - apply/esym; rewrite -(@eqR_mul2l (/ x)) //; last exact/nesym/eqP/ltR_eqF/invR_gt0. rewrite mulVR //; last exact/gtR_eqF. apply log_id_eq; first by apply mulR_gt0 => //; exact: invR_gt0. rewrite -(@eqR_mul2l x); last exact/eqP/gtR_eqF. rewrite {1}(mulRC _ y) Hxy2 mulRA mulRBr; congr (_ * _). field; exact/eqP/gtR_eqF. Qed.
imports: mathcomp(all_ssreflect ssralg all_algebra reals) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ln_facts logb fdist proba