proposition: Lemma invbumprowK r a : is_row r -> bump r a -> (invbumprow (bumped r a) (ins r a)) = (r, a).
proof: Proof. Proof using. rewrite /bump; move=> Hrow Hbump; have:= bump_bumprowE Hrow Hbump. elim: r Hrow Hbump => [_ /= | l0 r IHr /= /is_row_cons[Hl0 Hrow] Hbump]; first by rewrite ltxx. case: (ltP a l0) => Hal0. - by move=> [] <- <- /=; rewrite Hl0. - have {}Hbump: (a < last a r)%O. case: r {IHr Hl0 Hrow} Hbump Hal0 => [/= | //]; first exact: lt_le_trans. have H := bump_bumprowE Hrow Hbump. rewrite H => [][<- <-] /=. have:= head_ins_lt_bumped Hrow (bumped r a) Hbump; rewrite ltNge => /negbTE ->. by rewrite (IHr Hrow Hbump H). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab