proposition: Lemma dominate_inspos r1 r0 l : is_row r0 -> is_row r1 -> dominate r1 r0 -> bump r0 l -> inspos r0 l >= inspos r1 (bumped r0 l).
proof: Proof. Proof using. move=> Hrow0 Hrow1 /dominateP[Hsz Hdom] /= Hbump. case (ltnP (inspos r0 l) (size r1)) => Hpossz. - move/(_ _ Hpossz): Hdom; rewrite -/(bumped r0 l) => Hl1. apply: (inspos_leq_exP Hrow1). by rewrite /inspred /bumped (set_nth_default inh _ Hpossz) (set_nth_default inh _ (leq_trans Hpossz Hsz)). - by apply: (@leq_trans (size r1)); first exact: inspos_leq_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab