proposition: Lemma concaveEk1 (f : nat -> nat) (i k1 k2 : nat) : concave f -> f (i + k1 + k2) + f i <= f (i + k2) + f (i + k1).
proof: Proof. move=> fC; have [fI dfD] := fC. elim: k2 k1 i => [k1 i|k2 IHH k1 i]; first by rewrite !addn0 addnC. rewrite !addnS -(subnK (fI _)) -[X in _ <= X + _](subnK (fI _)). rewrite -addnA -[X in _ <= X]addnA leq_add //. by apply: (decreasingE dfD); rewrite addnAC leq_addr. Qed.
imports: mathcomp(all_ssreflect finmap)