proposition: Lemma log_concave_at_gt0W x y (t : {prob R}) : x < y -> 0 < x -> 0 < y -> concave_function_at log x y t.
proof: Proof. move=> xy x0 y0; rewrite /log /Log. apply concave_function_atN; [exact: ln_concave_at_gt0 | exact/ltRW/invR_gt0/ln2_gt0]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex