proposition: Lemma merge_sortedE l k : is_part l -> is_part k -> merge geq l k = sort geq (l ++ k).
proof: Proof. rewrite !is_part_sortedE => /andP[sortl _] /andP[sortk _]. apply (sorted_eq (leT := geq)) => //. - apply: merge_sorted => //. - exact: sort_sorted. - by rewrite perm_merge perm_sym perm_sort. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype