proposition: Lemma partdomsh_cons2 y1 y2 s t n1 n2 : partdomsh n1 n2 (y1 :: s) (y2 :: t) = (n1 <= n2) && (partdomsh (n1 + y1) (n2 + y2) s t).
proof: Proof. apply/partdomshP/andP => [H | [Hn /partdomshP Hdom] [|i]] /=; first split. - by have:= H 0; rewrite /= !addn0. - by apply/partdomshP => i; have:= H i.+1; rewrite /= !addnA. - by rewrite !addn0. - by rewrite !addnA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype