proposition: Lemma concaveEk f i k : concave f -> k <= i -> f (i - k) + f (i + k) <= (f i).*2.
proof: Proof. move=> [fI dfD]. elim: k => /= [kLi|k IH kLi]; first by rewrite subn0 addn0 addnn. have H : i - k.+1 <= i + k. by apply: leq_trans (leq_subr _ _) (leq_addr _ _). have fk1Lfk : f (i - k.+1) <= f (i - k). by apply/(increasingE fI)/leq_sub2l. have := leq_add (decreasingE dfD H) (IH (ltnW kLi)). rewrite /delta [f (i - k) + _]addnC addnA subnK ?fU // addnC. rewrite -subSn // subSS addnBAC // leq_subRL. by rewrite addnCA leq_add2l addnS. by apply: leq_trans fk1Lfk (leq_addr _ _). Qed.
imports: mathcomp(all_ssreflect finmap)