proposition: Lemma notbump : ~~bump = (l >= (last l Row))%O.
proof: Proof. Proof using. by rewrite /bump /= -leNgt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab