proposition: Lemma merge_cons x s t : is_part (x :: s) -> is_part t -> merge geq (x :: s) t = merge geq [:: x] (merge geq s t).
proof: Proof. move=> Hxs Ht. have Hs := is_part_consK Hxs. have Hx : is_part [:: x] by rewrite /= lt0n (part_head_non0 Hxs). rewrite (merge_sortedE Hxs Ht) (merge_sortedE Hx) ?merge_is_part //=. apply (sorted_eq (leT := geq)) => //; try exact: sort_sorted. by rewrite perm_sort perm_sym perm_sort perm_cons perm_merge. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype