proposition: Lemma fmerge_aux_exist f g i j n : exists2 k, k <= n & fmerge_aux f g i j n = minn (f (i + k)) (g (j + (n - k))).
proof: Proof. elim: n i j => /= [i j | n IH i j]; first by exists 0; rewrite //= !addn0. case: (leqP (g j) (f i)) => [gLf|fLg]; last first. by case: (IH i.+1 j) => k kLn ->; exists k.+1; rewrite // addnS subSS. case: (IH i j.+1) => [] [|k] kLn ->. by exists 0; rewrite // addn0 !subn0 addnS. by exists k.+1; rewrite ?(leq_trans kLn) // addSnnS -subSn. Qed.
imports: mathcomp(all_ssreflect finmap)