proposition: Lemma leq_sum_fmerge_conv f g k n : increasing f -> increasing g -> k <= n -> \sum_(i < n) fmerge f g i <= \sum_(i < k) f i + \sum_(i < n - k) g i.
proof: Proof. move=> fI gI; case: n => [|n kLn]. by case: k; rewrite // !big_ord0. rewrite -sum_fmerge_correct. exact: (sum_fmerge_aux_conv_correct 0 0 fI gI kLn). Qed.
imports: mathcomp(all_ssreflect finmap)