proposition: Lemma ins_leq i : i < size Row -> (nth l ins i <= nth l Row i)%O.
proof: Proof. Proof using HRow. rewrite -insE /insmin nth_set_nth /=. case eqP => [-> | _ _ //]. rewrite /mininspred /inspred; case (ltP l (last l Row)) => [Hcase | Hcase]. - by case (ex_minnP (ex_intro _ _ _)) => pos Hl _ _; exact: ltW. - by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab