proposition: Lemma fmergeE (f g : nat -> nat) n : increasing f -> increasing g -> fmerge f g n = \max_(i < n.+1) minn (f i) (g (n - i)).
proof: Proof. move=> fI gI. apply/eqP; rewrite /fmerge eqn_leq; apply/andP; split. case: (@fmerge_aux_exist f g 0 0 n) => // i1 i1Ln ->. by apply: (@leq_bigmax_cond _ _ _ (Ordinal (i1Ln : i1 < n.+1))). apply/bigmax_leqP => /= i _. by apply: fmerge_aux_correct; rewrite -1?ltnS. Qed.
imports: mathcomp(all_ssreflect finmap)