proposition: Lemma inspos_rcons l r b : (l < b)%O -> inspos r l = inspos (rcons r b) l.
proof: Proof. Proof using. by elim: r => [/= -> // | r0 r IHr]; rewrite rcons_cons /= => /IHr ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr