proposition: Lemma affine_functionP (f : T -> U) : affine f <-> convex_function f /\ concave_function f.
proof: Proof. split => [H | [H1 H2] p q t]; last first. by rewrite eqconv_le; split; [exact/H1|exact/H2]. split => p q t. - by rewrite /convex_function_at H; exact/leconvR. - by rewrite /concave_function_at/convex_function_at H; exact/leconvR. 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