proposition: Lemma nbump_bumprowE : ~~bump -> bumpRow = (None, ins).
proof: Proof. Proof using HRow. rewrite notbump -(insE HRow) (insrowE HRow). elim: Row HRow => [// | t0 r IHr] Hrow Hlast /=. case: (ltP l t0) => //= Ht0. - exfalso. have:= le_lt_trans (le_trans (head_leq_last_row Hrow) Hlast) Ht0. by rewrite ltxx. - have {}Hlast : (last l r <= l)%O by case: r Hlast {IHr Hrow}. 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