proposition: Lemma sorted_is_part p : is_part p -> sorted geq p.
proof: Proof. case: p => [// | p0 p] /= /andP[]. elim: p p0 => [// | p1 p IHp] /= p0 -> /andP[] /=. exact: IHp. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule