proposition: Lemma is_part_pad0 n p : is_part p -> sorted geq (pad 0 n p).
proof: Proof. have Hpath x i : path geq x (nseq i 0). by case: i => [// | i] /=; elim: i. case: p => [_ | p0 p]; case: n => [| n /=] //=. rewrite cats0 -/(sorted geq (p0 :: p)) -/(is_part (p0 :: p)). exact: sorted_is_part. rewrite subSS. elim: p p0 n => [| p1 p IHp] /= p0 n; first by move=> _; exact: Hpath. move=> /andP[-> {}/IHp Hrec /=]. case: n => [| n /=]; first by move/(_ 0): Hrec; rewrite !sub0n. by rewrite subSS; exact: Hrec. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule