proposition: Lemma conj_leqE sh : is_part sh -> forall i j, (nth 0 sh i <= j) = (nth 0 (conj_part sh) j <= i).
proof: Proof. by move=> Hpart i j; rewrite leqNgt [RHS]leqNgt (conj_ltnE Hpart). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype