proposition: Lemma partdomsh_cons2E y s t n1 n2 : partdomsh n1 n2 (y :: s) (y :: t) = partdomsh n1 n2 s t.
proof: Proof. rewrite partdomsh_cons2 ![_ + y]addnC partdomsh_add andbC. case: (boolP (partdomsh _ _ _ _)) => //= /partdomshP/(_ 0). by rewrite !take0 /= !addn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype