proposition: Lemma inspredN_lt_inspos i : i < pos -> ~~ (inspred i).
proof: Proof. Proof using. by rewrite /inspred -leNgt; apply: nth_lt_inspos. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab