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