proposition: Lemma sum_fmerge_aux_exist f g i j n : exists2 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. elim: n i j => /= [i j | n IH i j]. rewrite /minn; case: leqP => [gLf|fLg]. by exists 0; rewrite // big_ord_recl !big_ord0 !(add0n, addn0). by exists 1; rewrite // subnn big_ord_recl !big_ord0 !(add0n, addn0). case: (leqP (g j) (f i)) => [gLf|fLg]. case: (IH i j.+1) => k kLn ->. exists k; first by apply: leq_trans kLn _. rewrite (subSn kLn) big_ord_recl addn0 addnCA. by congr (_ + (_ + _)); apply: eq_bigr => l _; rewrite addnCA. case: (IH i.+1 j) => k kLn ->; exists k.+1; first by apply: leq_trans kLn _. rewrite big_ord_recl addn0 subSS -addnA. by congr (_ + (_ + _)); apply: eq_bigr => l _; rewrite addnCA. Qed.
imports: mathcomp(all_ssreflect finmap)