proposition: Lemma nth_conjE sh r c : is_part sh -> c != 0 -> (nth 0 (conj_part sh) r == c) = (nth 0 sh c <= r < nth 0 sh c.-1).
proof: Proof. move=> Hpart. case: c => //= c _. rewrite (conj_leqE Hpart) (conj_ltnE Hpart) /=. apply/idP/idP. - by move/eqP ->; rewrite !leqnn. - by move=> H; apply/eqP; exact: anti_leq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype