proposition: Lemma filter_le_shiftn sh t : [seq x - sh | x <- [seq sh + i | i <- t] & sh <= x] = t.
proof: Proof. by elim: t => [// | l0 r IHt] /=; rewrite leq_addr /= addKn IHt. 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