proposition: Theorem Greene_row_invar_plactic u v : u =Pl v -> forall k, Greene_row u k = Greene_row v k.
proof: Proof. Proof using. move=> Hpl k. move: v Hpl; apply: gencongr_ind; first exact: erefl. move=> a b1 c b2 -> {u} /plactruleP[]. - exact: Greene_row_invar_plact1. - exact: Greene_row_invar_plact1i. - exact: Greene_row_invar_plact2. - exact: Greene_row_invar_plact2i. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene