proposition: Lemma bump_bumprowE : bump -> bumpRow = (Some bumped, ins).
proof: Proof. Proof using HRow. rewrite /bumped -(insE HRow) (insrowE HRow). elim: Row HRow => [// | t0 r IHr] Hrow /= Hlast; first by rewrite bump_nil in Hlast. case: (ltP l t0) => //=. move: Hlast => /bump_tail H{}/H Hlast. by rewrite (IHr (is_row_consK Hrow) Hlast). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab