proposition: Lemma sum_fmerge_exist f g n : exists2 k, k <= n & \sum_(i < n) fmerge f g i = \sum_(i < k) f i + \sum_(i < n - k) g i.
proof: Proof. case: n => [|n]; first by exists 0; rewrite // !big_ord0. case: (sum_fmerge_aux_exist f g 0 0 n) => k kLn sE. by exists k; rewrite // -sum_fmerge_correct [LHS]sE. Qed.
imports: mathcomp(all_ssreflect finmap)