proposition: Lemma concavef_at_onem x y (t : {prob R}) f : (0 < x -> 0 < y -> x < y -> concave_function_at f x y t -> concave_function_at f y x (Prob.p t).~%:pr)%coqR.
proof: Proof. move=>x0 y0 xy; rewrite/concave_function_at/convex_function_at. rewrite !conv_leoppD !leoppP/=. rewrite !avgRE /= onemK. by rewrite addRC [in X in leconv _ X -> _]addRC. 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