proposition: Lemma insrowE : insmin = insrow Row l.
proof: Proof. Proof using HRow. rewrite /insmin insposE. elim: Row HRow => [// | l0 r IHr] Hrow /=. by case: (ltP l l0) => _ //=; rewrite (IHr (is_row_consK Hrow)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab