fact: Fixpoint sum_fmerge_aux (f g : nat -> nat) i j n := if n is n1.+1 then if f i < g j then f i + sum_fmerge_aux f g i.+1 j n1 else g j + sum_fmerge_aux f g i j.+1 n1 else minn (f i) (g j).
imports: mathcomp(all_ssreflect finmap)