proposition: Lemma sum_fmerge_aux_correct f g n i j : sum_fmerge_aux f g i j n = \sum_(k < n.+1) fmerge_aux f g i j k.
proof: Proof. elim: n i j => //= [i j|n IH i j]; first by rewrite big_ord_recr big_ord0. by rewrite big_ord_recl /= /minn; case: leqP; rewrite IH. Qed.
imports: mathcomp(all_ssreflect finmap)