proposition: Lemma bump_dominate r1 r0 l : is_row r0 -> is_row r1 -> bump r0 l -> dominate r1 r0 -> dominate (ins r1 (bumped r0 l)) (ins r0 l).
proof: Proof. Proof using. move=> Hrow0 Hrow1 Hbump Hdom; have:= Hdom => /dominateP[Hsize Hlt]. have Hsize' : size (ins r1 (bumped r0 l)) <= size (ins r0 l). rewrite (bump_size_ins Hrow0 Hbump) {1}/ins size_set_nth /maxn. case (ltnP (inspos r1 (bumped r0 l)).+1 (size r1)) => [// | _]. apply: (@leq_ltn_trans (inspos r0 l)); first exact: dominate_inspos. exact: bump_inspos_lt_size. apply/dominateP; split; first exact Hsize'. move=> i Hi; rewrite (set_nth_default (bumped r0 l) inh Hi) (set_nth_default l inh (leq_trans Hi Hsize')). rewrite /ins; have:= dominate_inspos Hrow0 Hrow1 Hdom Hbump. set pos0 := inspos r0 _; set pos1 := inspos r1 _. move=> Hpos; rewrite !nth_set_nth /=. case eqP => [Hipos0 | /eqP Hipos0]; case eqP => [Hipos1 | /eqP Hipos1]. - exact: lt_bumped. - apply: (lt_le_trans (lt_bumped Hbump)); move Hl0 : (bumped r0 l) => l0. rewrite -Hipos0 in Hpos => {Hrow0 Hlt Hdom Hsize Hbump Hipos0}. rewrite /pos1 in Hipos1 Hpos; rewrite Hl0 in Hipos1 Hi Hpos => {pos1 pos0 Hl0}. have:= is_row_ins Hrow1 l0 => /is_rowP Hrowins. have {1}-> : l0 = nth l0 (ins r1 l0) (inspos r1 l0) by rewrite nth_set_nth /= eq_refl. have -> : nth l0 r1 i = nth l0 (ins r1 l0) i by rewrite nth_set_nth /= (negbTE Hipos1). by apply: Hrowins; rewrite Hpos. - apply: (@le_lt_trans _ T l); last exact: lt_bumped. by subst pos0; apply: nth_lt_inspos; rewrite ltn_neqAle Hipos0 /= Hipos1. - case (ltnP i (size r1)) => Hsz. * rewrite (set_nth_default inh _ Hsz) (set_nth_default inh _ (leq_trans Hsz Hsize)). exact: Hlt. * exfalso; case (boolP (bump r1 (bumped r0 l))) => [ | Hnbump]. - move/bump_size_ins => H; rewrite (H Hrow1) in Hi. by have:= leq_ltn_trans Hsz Hi; rewrite ltnn. - have:= Hnbump; move/nbump_ins_rconsE => Heq. rewrite (Heq Hrow1) size_rcons ltnS in Hi. have {Hsz}Hi : (i == size r1) by rewrite eqn_leq Hi Hsz. rewrite /pos1 (nbump_inspos_eq_size Hrow1 Hnbump) in Hipos1. by rewrite Hi in Hipos1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab