proposition: Lemma Schur0 (sh : 'P_0) : Schur sh = 1.
proof: Proof. Proof using. rewrite Schur_tabsh_readingE (eq_bigl (xpred1 [tuple])); first last. by move=> i /=; rewrite tuple0 [RHS]eq_refl val_intpartn0. by rewrite big_pred1_eq big_nil. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau