proposition: Lemma sum_fmerge_aux_conv_correct f g i j n : increasing f -> increasing g -> (forall k, k <= n.+1 -> sum_fmerge_aux f g i j n <= \sum_(l < k) f (i + l) + \sum_(l < n.+1 - k) g (j + l)).
proof: Proof. move=> fI gI. elim: n i j => /= [i j [_|[_|]]//|n IH i j k kLn]. - by rewrite big_ord_recr !big_ord0 /= !addn0 !add0n geq_minr. - by rewrite big_ord_recr !big_ord0 /= !addn0 !add0n geq_minl. case: leqP => [gLf|fLg]. move: kLn; case: ltngtP => // [kLn _ |-> _]; last first. rewrite subnn big_ord0 addn0 big_ord_recl addn0 /=. apply: leq_add => //. rewrite /bump /=. apply: leq_trans (IH _ _ _ (leqnn _)) _. rewrite subnn big_ord0 addn0 leq_sum // => l _. by apply: increasingE; rewrite // addnCA leq_addl. rewrite subSn // big_ord_recl addn0 addnCA leq_add2l. apply: leq_trans (IH _ _ _ (kLn : k <= n.+1)) _. rewrite leq_add2l leq_sum // => l _. by rewrite increasingE //= /bump addnCA add1n. move: kLn; case: ltngtP => // [kLn _ |-> _]; last first. rewrite subnn big_ord0 addn0 big_ord_recl addn0 /= leq_add2l /bump /=. apply: leq_trans (IH _ _ _ (leqnn _)) _. rewrite subnn big_ord0 addn0 leq_sum // => l _. by rewrite increasingE // addnCA add1n. case: k kLn => [_|k kLn]; last first. rewrite subSS. apply: leq_trans (leq_add (leqnn _) (IH i.+1 j k _)) _ . by rewrite -ltnS ltnW. rewrite addnA leq_add2r big_ord_recl addn0 leq_add2l leq_sum // => l _. by rewrite addnCA. rewrite big_ord0 add0n subn0. apply: leq_trans (leq_add (leqnn _) (IH i.+1 j 0 isT)) _ . rewrite big_ord0 add0n subn0 [X in _ <= X]big_ord_recr addnC leq_add //. apply: leq_trans (ltnW fLg) _. by rewrite increasingE // leq_addr. Qed.
imports: mathcomp(all_ssreflect finmap)