proposition: Lemma size_ins_sup : size ins <= (size Row).+1.
proof: Proof. Proof using. rewrite /ins size_set_nth maxnC /maxn ltnS. case (leqP (size Row) pos) => [H | _]; last exact: leqnSn. exact: inspos_leq_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab