proposition: Lemma insE : insmin = ins.
proof: Proof. Proof using HRow. by rewrite /insmin /ins insposE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab