fact: Definition fconvex_strict := forall (x y: E) (t: oprob), x <> y -> f (x <|t|> y) < EFin (t : R_ringType) * f x + EFin (onem t)%R * f y.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals