proposition: Lemma convexE f : increasing f -> (forall i, (f i.+1).*2 <= f i + f i.+2) -> convex f.
proof: Proof. move=> fI fH; split => // i. rewrite /delta. rewrite -(leq_add2r (f i.+1 + f i)) [_ + f i]addnC addnA subnK //. by rewrite addnn [f i + _]addnC addnA subnK // addnC. Qed.
imports: mathcomp(all_ssreflect finmap)