proposition: Lemma is_row_ins : is_row ins.
proof: Proof. Proof using HRow. move: HRow; rewrite -insE /insmin /mininspred => Hrow. case (ltP l (last l Row)) => Hlast. - case (ex_minnP (ex_intro _ _ _)) => pos. by rewrite /inspred; exact: is_row_set_nth. - by rewrite rcons_set_nth; exact: is_row_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab