proposition: Theorem Greene_row_tab_eq_shape (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (t1 : seq (seq T1)) (t2 : seq (seq T2)) : is_tableau t1 -> is_tableau t2 -> (forall k, Greene_row (to_word t1) k = Greene_row (to_word t2) k) -> (shape t1 = shape t2).
proof: Proof. move=> Htab1 Htab2 Heq. have Hsh1 := is_part_sht Htab1; have Hsh2 := is_part_sht Htab2. apply: (sumn_take_inj Hsh1 Hsh2). move=> k. rewrite -(Greene_row_tab k Htab1) -(Greene_row_tab k Htab2). exact: Heq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype