proposition: Lemma R_convex_functionB f (g : T -> R) : convex_function f -> concave_function g -> convex_function (fun x => f x - g x)%coqR.
proof: Proof. move=> Hf Hg p q t. rewrite /convex_function_at /= avgRE 2!mulRBr addRAC addRA. rewrite -addR_opp -addRA; apply: (leR_add _ _ _ _ (Hf _ _ _)). by rewrite -2!mulRN addRC; exact: (R_convex_functionN Hg). 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