proposition: Lemma partdomsh_add y n1 n2 s1 s2 : partdomsh (y + n1) (y + n2) s1 s2 = partdomsh n1 n2 s1 s2.
proof: Proof. rewrite/partdomsh; apply eq_all => i. by rewrite -!addnA leq_add2l. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype