proposition: Lemma stdtab_get_tabNE t : is_stdtab t -> forall rc1 rc2, in_shape (shape t) rc1 -> in_shape (shape t) rc2 -> rc1 != rc2 -> get_tab t rc1 != get_tab t rc2.
proof: Proof. move=> /andP[_ /std_uniq]. elim: t => [_ | t0 t /= IHt Huniq] [r1 c1] [r2 c2]. by rewrite /in_shape /= nth_default //. move: Huniq; rewrite to_word_cons cat_uniq => /and3P[Ht /hasPn Htt0 Ht0]. rewrite /in_shape /get_tab; case: r1 r2 => [| r1] [| r2]/= Hc1 Hc2. - by apply /contra; rewrite [(0, _) == _]/eq_op/= (nth_uniq _ Hc1 Hc2 Ht0). - move=> _; have:= mem_nth inh Hc1 => /Htt0; apply contra => /eqP ->. move: Hc2; rewrite -/(get_tab _ (_, _)) -/(in_shape _ (_, _)). exact: mem_to_word. - move=> _; have:= mem_nth inh Hc2 => /Htt0; apply contra => /eqP <-. move: Hc1; rewrite -/(get_tab _ (_, _)) -/(in_shape _ (_, _)). exact: mem_to_word . - rewrite {1}/eq_op/= eqSS -[~~ ((r1 == r2) && (c1 == c2))]/((_, _) != (_, _)). exact: IHt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau