proposition: Lemma convex_in_bothP : convex_in_both <-> forall a0 a1 b0 b1 t, f (a0 <| t |> a1) (b0 <| t |> b1) <= f a0 b0 <| t |> f a1 b1.
proof: Proof. split => [H a0 a1 b0 b1 t | H]; first by move: (H (a0,b0) (a1,b1) t); rewrite /convex_function_at /uncurry. by case => a0 b0 [a1 b1] t; move:(H a0 a1 b0 b1 t). 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