proposition: Lemma conj_ltnE sh : is_part sh -> forall i j, nth 0 sh i > j = (nth 0 (conj_part sh) j > i).
proof: Proof. move=> Hpart. rewrite -/(in_shape sh _) -/(in_shape (conj_part sh) _). exact: in_conj_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype