proposition: Lemma R_concave_functionB f (g : T -> R) : concave_function f -> convex_function g -> concave_function (fun x => f x - g x)%coqR.
proof: Proof. move=> Hf Hg. rewrite (_ : (fun _ => _) = (fun x => - (g x - f x)))%coqR; last first. by apply/funext => x; rewrite oppRB. exact/R_concave_functionN/R_convex_functionB. 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