proposition: Lemma dominateK_inspos r1 r0 l0 : is_row r0 -> is_row r1 -> dominate (ins r1 (bumped r0 l0)) (ins r0 l0) -> bump r0 l0 -> inspos r0 l0 >= inspos r1 (bumped r0 l0).
proof: Proof. Proof using. move Hl1 : (bumped r0 l0) => l1; rewrite /bumped in Hl1. move=> Hrow0 Hrow1 /dominateP[Hsz Hdom] /= Hbump. case (leqP (inspos r1 l1) (inspos r0 l0)) => [// | Habs]. have Hpos1 := inspos_lt_size_ins r1 l1. have:= leq_trans Hpos1 Hsz; rewrite (bump_size_ins Hrow0 Hbump) => Hpos0. move: Hrow0 => /is_rowP Hrow0. have: inspos r0 l0 <= inspos r1 l1 < size r0 by rewrite (ltnW Habs). move/(Hrow0 l0); rewrite {Hrow0} Hl1 => H1. move/(_ _ Hpos1): Hdom. rewrite (set_nth_default l1 inh Hpos1) (set_nth_default l0 inh (leq_trans Hpos1 Hsz)). rewrite /ins !nth_set_nth /= (gtn_eqF Habs) eq_refl. by move/(le_lt_trans H1); rewrite ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab