proposition: Theorem Greene_col_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_col (to_word t1) k = Greene_col (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. suff : conj_part (shape t1) = conj_part (shape t2). move=> H; rewrite -(conj_partK Hsh1) -(conj_partK Hsh2). by rewrite H (conj_partK Hsh2). apply: (sumn_take_inj (is_part_conj Hsh1) (is_part_conj Hsh2)). move=> k. rewrite -(Greene_col_tab k Htab1) -(Greene_col_tab k Htab2). exact: Heq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype