proposition: Lemma inspred_any_bump i : inspred i -> bump.
proof: Proof. Proof using HRow. rewrite /inspred /= /bump; have:= HRow. elim: Row i => [/= | l0 r IHr] i /=; first by case: i. case: i => [|i] /is_row_cons[Hhead Hrow]. - case: r {IHr} Hhead Hrow => [// |l1 r] /= Hl0l1. move/head_leq_last_row => Hlast Hll0. exact: lt_le_trans Hll0 (le_trans Hl0l1 Hlast). - by move/(IHr _ Hrow); case r => //; rewrite ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab