proposition: Lemma nbump_insposE : ~~bump -> mininspred = pos.
proof: Proof. Proof using HRow. move=> Hbump; rewrite (nbump_mininspredE Hbump). move: Hbump; rewrite notbump. elim: Row HRow => [// | l0 r IHr] Hrow /= Hlast. case: (ltP l l0) => [Hll0 | _]. * exfalso => {IHr}. have:= le_lt_trans (le_trans (head_leq_last_row Hrow) Hlast) Hll0. by rewrite ltxx. * move: Hrow => /is_row_consK {}/IHr. case: r Hlast => [// | l1 r] /= Hlast. by case: (ltP l l1) => _ /(_ Hlast) ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab