proposition: Lemma fmerge_aux_correct f g i j n : increasing f -> increasing g -> (forall k, k <= n -> minn (f (i + k)) (g (j + (n - k))) <= fmerge_aux f g i j n).
proof: Proof. move=> fI gI. elim: n i j => /= [i j [|] // _|n IH i j k kLn]. by rewrite !addn0. case: leqP => [gLf|fLg]. move: kLn; rewrite leq_eqVlt => /orP[/eqP->|kLn]. rewrite subnn addn0 (minn_idPr _); last first. by rewrite (leq_trans gLf) // increasingE // leq_addr. apply: leq_trans (IH _ _ _ (leqnn _)). rewrite subnn addn0 leq_min increasingE // andbT (leq_trans gLf) //. by rewrite increasingE // leq_addr. by rewrite subSn // -addSnnS IH. case: k kLn => [_ | k kLn]. rewrite addn0 subn0 (minn_idPl _); last first. by rewrite (leq_trans (ltnW fLg)) // increasingE // leq_addr. apply: leq_trans (IH i.+1 j 0 isT). rewrite addn0 leq_min increasingE //= (leq_trans (ltnW fLg)) //. by rewrite increasingE // leq_addr. by rewrite subSS -addSnnS IH. Qed.
imports: mathcomp(all_ssreflect finmap)