proposition: Theorem RSmapinv2K pair : is_RSpair pair -> RSmap (RSmapinv2 pair) = pair.
proof: Proof. Proof using. rewrite /is_RSpair /RSmap /RSmapinv2; case: pair => [tab yam] /and3P[]. elim: yam tab => [[] // | row yam IHyam] tab Htab Hyam Hshape /=. have:= is_rem_corner_yam Hyam; rewrite -(eqP Hshape) => Hcorn. have Hnnil : (tab != [::]). move: Hshape; case tab => //= /eqP /(congr1 size). rewrite /= size_incr_nth. move: (size (evalseq yam)) => n. by case (ltnP row n) => //= /ltn_predK <-. have:= instabnrowinvK Htab Hnnil Hcorn. have:= is_tableau_instabnrowinv1 Htab Hcorn. have:= shape_instabnrowinv1 Hyam Hshape. case Hinvins: (invinstabnrow tab row) => [tin l] /= Hshapetin Htabtin. rewrite rev_rcons /=. move: Hyam => /= /andP[Hincr Hyam]. by have:= IHyam tin Htabtin Hyam Hshapetin => /= -> ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab