proposition: Lemma div_diff_ub x y : 0 <= x -> (y = 0 -> x = 0) -> 0 <= y -> x * (log (y / x)) <= (y - x) * log (exp 1).
proof: Proof. move=> x0 yx /leR_eqVlt[/esym|] y0. - by move: (yx y0) => ->; rewrite y0 subRR 2!mul0R. - case/leR_eqVlt : x0 => [/esym ->|x0]. + rewrite mul0R subR0; apply mulR_ge0; [exact: ltRW | exact: log_exp1_Rle_0]. + rewrite (_ : y - x = x * (y / x - 1)); last first. by rewrite mulRDr mulRCA mulRV ?mulR1 ?mulRN1 //; exact/gtR_eqF. rewrite -mulRA; apply (leR_wpmul2l (ltRW x0)). by apply/log_id_cmp/mulR_gt0 => //; exact/invR_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg all_algebra reals) Reals mathcomp(Rstruct) ssrR realType_ext Reals_ext ln_facts logb fdist proba