proposition: Lemma head_ins_lt_bumped i : bump -> (head i ins < bumped)%O.
proof: Proof. Proof using HRow. move=> Hbump; have:= is_row_ins HRow l => /is_rowP Hrowins. rewrite -nth0 (set_nth_default l i (size_ins_non_0 _ _)). apply: (@le_lt_trans _ T (nth l ins inspos)). + apply: Hrowins. rewrite /= (bump_size_ins HRow Hbump). exact: bump_inspos_lt_size. + rewrite /ins nth_set_nth /= eq_refl. exact: lt_bumped. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab