proposition: Lemma convexf_at_onem x y (t : {prob R}) f : (0 < x -> 0 < y -> x < y -> convex_function_at f x y t -> convex_function_at f y x (Prob.p t).~%:pr)%coqR.
proof: Proof. move=> x0 y0 xy H; rewrite /convex_function_at. rewrite [in X in leconv _ X]avgRE /= onemK addRC. rewrite /convex_function_at !avgRE in H. rewrite avgRE /= onemK addRC. by apply: (leR_trans H); rewrite addRC; apply/RleP; rewrite lexx. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist