proposition: Lemma partdomsh_merge1 n1 n2 x t1 t2 : is_part t1 -> is_part t2 -> partdomsh n1 n2 t1 t2 -> partdomsh n1 n2 (merge geq [:: x] t1) (merge geq [:: x] t2).
proof: Proof. move=> Ht1 Ht2 /partdomshP Hdom; apply/partdomshP => i. case: i => [|i]. - by move/(_ 0): Hdom; rewrite /= !take0. - rewrite !sumn_take_merge // !addn_maxr. rewrite ![_ + (x + _)]addnC -![x + _ + _]addnA ![sumn _ + _]addnC. by rewrite geq_max !leq_max ?leq_add2l !Hdom /= orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype