proposition: Lemma bump_dominateK r1 r0 l0 : is_row r0 -> is_row r1 -> bump r0 l0 -> dominate (ins r1 (bumped r0 l0)) (ins r0 l0) -> dominate r1 r0.
proof: Proof. Proof using. move=> Hrow0 Hrow1 Hbump0 Hdom; have:= Hdom => /dominateP[Hsize Hlt]. have:= dominateK_inspos Hrow0 Hrow1 Hdom Hbump0 => Hpos. move Hl1 : (bumped r0 l0) => l1; rewrite Hl1 in Hdom Hsize Hlt Hpos. rewrite /bumped in Hl1. have Hsize' : size r1 <= size r0. move: Hsize; rewrite (bump_size_ins Hrow0 Hbump0). by apply/leq_trans; exact: size_ins_inf. apply/dominateP; split; first exact: Hsize'. move=> i Hi; have Hi' := leq_trans Hi (size_ins_inf Hrow1 l1). rewrite (set_nth_default l1 inh Hi) (set_nth_default l0 inh (leq_trans Hi Hsize')). case/altP: (i =P inspos r1 l1) => Hipos1. - have:= nth_inspos_ins r1 l1; rewrite -Hipos1. have:= Hlt i Hi'. rewrite (set_nth_default l0 inh (leq_trans Hi' Hsize)) (set_nth_default l1 inh Hi'). rewrite {1}Hipos1 {1}/ins nth_set_nth {1}Hipos1 /=. case/altP: (i =P inspos r0 l0) => [Hipos0 _| Hipos0]. + rewrite {2}Hipos0 Hl1 => <-; rewrite Hipos1 nth_inspos_ins. case (boolP (bump r1 l1)) => Hbump; last by move: Hi; rewrite Hipos1 (nbump_inspos_eq_size Hrow1 Hbump) ltnn. by have:= inspred_mininspred Hbump; rewrite (insposE Hrow1) /inspred. + rewrite -{1}Hipos1 (negbTE Hipos0) nth_inspos_ins => Hlt1 Heqins. rewrite -Hipos1 in Hlt1. apply: (lt_le_trans Hlt1); rewrite -{1}Heqins. exact: ins_leq. - case/altP: (i =P inspos r0 l0) => Hipos0. + rewrite Hipos0 Hl1. have:= contra (@lt_inspos_nth r1 Hrow1 l1 _ Hi). by rewrite -leqNgt -ltNge Hipos0; apply. + have:= Hlt _ Hi'. rewrite (set_nth_default l0 inh (leq_trans Hi' Hsize)) (set_nth_default l1 inh Hi'). by rewrite !/ins !nth_set_nth /= (negbTE Hipos0) (negbTE Hipos1). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab