proposition: Lemma sumn_union_part l k : sumn (merge geq l k) = sumn l + sumn k.
proof: Proof. have:= perm_merge geq l k => /permPl/perm_sumn ->. by rewrite sumn_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype