proposition: Lemma lt_inspos_nth i : i < size Row -> (nth l Row i <= l)%O -> i < pos.
proof: Proof. Proof using HRow. move: HRow; move=> /is_rowP Hrow Hi Hnthi; rewrite -insposE /mininspred /inspred. case (ltP l (last l Row)) => [Hlt | //]. case (ex_minnP (ex_intro _ _ _)) => pos /(le_lt_trans Hnthi) H1 _. move/(_ l pos i): Hrow => H2. have {H2} /contra : pos <= i -> (nth l Row pos <= nth l Row i)%O. by move=> H; apply: H2; apply/andP. by rewrite -ltnNge -ltNge; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab