proposition: Lemma filter_gt_shiftn sh t : [seq x <- [seq sh + i | i <- t] | gtn sh x] = [::].
proof: Proof. by elim: t => [// | l0 r /= ->] /=; rewrite ltnNge leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur