proposition: Lemma is_stdtab_conj t : is_stdtab t -> is_stdtab (conj_tab t).
proof: Proof. move=> Hstdtab. have:= Hstdtab; rewrite /is_stdtab => /andP[Htab Hstd]. have Hp := is_part_sht Htab; have Hc := is_part_conj Hp. apply/andP; split. - apply/is_tableauP; split. rewrite size_conj_tab => i Hi. have:= nth_part_non0 Hc Hi. apply contra => /eqP. by rewrite -shape_conj_tab nth_shape => ->. - move=> i; apply/(is_rowP inh) => j1 j2 /andP[Hj]. rewrite -nth_shape shape_conj_tab -(conj_ltnE Hp) nth_shape => Hjsz. rewrite -!/(get_tab _ (_, _)) !(get_conj_tab Hp). have:= Htab => /is_tableauP[_ _ Hdom]. move: Hj; rewrite leq_eqVlt => /orP[/eqP -> // | ] {}/Hdom/dominateP[_ Hdom]. by have /= := ltW (Hdom _ Hjsz); apply. - move=> j1 j2 Hj. apply/dominateP; split. + rewrite -!nth_shape shape_conj_tab. by move: Hc => /is_part_ijP[_]; apply; apply: ltnW. + move=> i; rewrite -!nth_shape shape_conj_tab -(conj_ltnE Hp) => Hj2. rewrite -!/(get_tab _ (_, _)) !(get_conj_tab Hp) /get_tab. have:= Htab => /is_tableauP[_ Hrow _]. rewrite lt_def (is_rowP inh _ (Hrow i)); first last. by rewrite (ltnW Hj) -nth_shape Hj2. rewrite -/(in_shape _ _) in Hj2. rewrite andbT -!/(get_tab _ (_, _)); apply (stdtab_get_tabNE Hstdtab). * exact: Hj2. * exact: (in_part_le (is_part_sht Htab) Hj2 (leqnn _) (ltnW Hj)). * by rewrite xpair_eqE eq_refl /= (gtn_eqF Hj). - apply/is_stdP => n. rewrite size_to_word /size_tab shape_conj_tab sumn_conj_part -/(size_tab _) -size_to_word => /is_stdP/=/(_ Hstd) Hn. have:= Hn; rewrite -index_mem; have := nth_index inh Hn. move: (index _ _) => pos <- {Hn} Hpos. move: Hpos; rewrite size_to_word /size_tab -sumn_rev /shape -map_rev -/(shape _). move=> Htmp; have:= reshape_offsetP Htmp; move/reshape_indexP : Htmp. rewrite (nth_flatten inh (rev t) pos) shape_rev size_rev size_map => Hpos. do !rewrite nth_rev ?size_map //. rewrite -/(get_tab _ (_, _)) -/(in_shape _ (_, _)) -(get_conj_tab Hp). rewrite (in_conj_part Hp) -shape_conj_tab {Hpos}. exact: mem_to_word. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau