proposition: Lemma sum_fmerge_conv f g n : increasing f -> increasing g -> \sum_(i < n) (fmerge f g) i = conv (fun n => \sum_(i < n) f i) (fun n => \sum_(i < n) g i) n.
proof: Proof. move=> fI gI. apply/eqP; rewrite eqn_leq; apply/andP; split; last first. case: (sum_fmerge_exist f g n) => k kLn ->. by apply: (bigmin_inf _ (leqnn _)). apply/bigmin_leqP => k kLn. by apply: leq_sum_fmerge_conv. Qed.
imports: mathcomp(all_ssreflect finmap)