proposition: Theorem rembig_RS a v : {i | RS (a :: v) = append_nth (RS (rembig (a :: v))) (maxL a v) i}.
proof: Proof. Proof using. by exists (last_big (RS (a :: v)) (maxL a v)); exact: rembig_RS_last_big. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr