proposition: Lemma partdomsh_merge n1 n2 s t1 t2 : is_part s -> is_part t1 -> is_part t2 -> partdomsh n1 n2 t1 t2 -> partdomsh n1 n2 (merge geq s t1) (merge geq s t2).
proof: Proof. elim: s => [//| s0 s IHs] Hs0s Ht1 Ht2 Hdom. have Hs := is_part_consK Hs0s. rewrite !(merge_cons Hs0s) //. apply partdomsh_merge1; try exact: merge_is_part. exact: IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype