proposition: Lemma log_concave : concave_function_in Rpos_interval log.
proof: Proof. move=> x y t; rewrite !classical_sets.in_setE => Hx Hy. exact: log_concave_at_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex