proposition: Lemma convex_conv f g : convex f -> convex g -> convex (conv f g).
proof: Proof. move=> [fI dfI] [gI dgI]; split; first by apply: increasing_conv. apply: increasing_ext => [i|]; first by apply/sym_equal/delta_conv. by apply: increasing_fmerge. Qed.
imports: mathcomp(all_ssreflect finmap)