proposition: Lemma bumprow_rcons r l : is_row (rcons r l) -> bumprow r l = (None, rcons r l).
proof: Proof. Proof using. move=> Hrow; have:= is_row_last Hrow; rewrite leNgt => Hnbump. move/is_row_rconsK: Hrow => Hr. by rewrite (nbump_bumprowE Hr Hnbump) (nbump_ins_rconsE Hr Hnbump). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab