proposition: Lemma conj_partK sh : is_part sh -> conj_part (conj_part sh) = sh.
proof: Proof. elim: sh => //= s0 sh IHsh /andP[Hhead Hpart]. case: (sh =P [::]) => Hsh. - move: Hhead; rewrite Hsh /=; exact: conj_nseq. - rewrite conj_part_ind //=; first by rewrite IHsh. + apply/contra_notN: Hsh => /eqP. case: sh Hpart {IHsh Hhead} => //= s1 s. case: s1 => [/andP[] | s1 _]; first by rewrite leqn0 => /part_head0F ->. by case: (conj_part s). + exact: is_part_conj. + rewrite size_conj_part //=. by move: Hhead Hsh; case sh. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype