proposition: Lemma bump_tail l0 r l : bump (l0 :: r) l -> (l0 <= l -> bump r l)%O.
proof: Proof. Proof using. rewrite /bump /= => Hbump Hll0. case: r Hbump => [/= H1 | //]. by exfalso; have:= lt_le_trans H1 Hll0; rewrite ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab