proposition: Lemma log_concave_at_gt0 x y (t : {prob R}) : 0 < x -> 0 < y -> concave_function_at log x y t.
proof: Proof. move=> x0 y0. case/boolP : (x < y)%mcR => [/RltP xy|]. exact: log_concave_at_gt0W. rewrite -leNgt le_eqVlt => /predU1P[->|yx]. exact: concave_function_atxx. rewrite (probK t); apply: concavef_at_onem => //. exact/RltP. by apply: log_concave_at_gt0W => //; exact/RltP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex