proposition: Lemma insposE : mininspred = pos.
proof: Proof. Proof using HRow. by case (boolP bump); [exact: bump_insposE | exact: nbump_insposE]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab