proposition: Lemma partdom_consK x s1 s2 : partdom (x :: s1) (x :: s2) -> partdom s1 s2.
proof: Proof. rewrite /partdom partdomsh_cons2 add0n leqnn /=. by rewrite -(addn0 x) partdomsh_add. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype