Library Combi.Combi.stdtab: Standard Tableaux
Standard Tableaux
- append_nth t b i == t with b appended to its i-th row
- is_stdtab t == t is a *standard tableau* that is a tableau whose row reading is a standard word
- last_big t b == the index of the first row of t which ends with b
- remn t == remove the largest entry ie n from a standard tableau of size n
- conj_tab t == the conjugate standard tableau of t (this is indeed a tableau when t is itself a standard tableau.
- stdtab_of_yam y == the standard tableau associated to y
- yam_of_stdtab t == the Yamanouchi words associated to t
- is_stdtab_of_shape sh == a predicate for standard tableau of shape sh.
- stdtabsh sh == a sigma type for is_stdtab_of_shape sh where sh is an
integer partition (of type intpart). This is canonically a
finType.
- is_stdtab_of_n n == a predicate for standard tableau of size n
- stdtabn n == a sigma type for is_stdtab_of_n n. This is canonically a
finType.
- shape_deg t == if t is of type stdtabn n, the shape of t in the
sigma type 'P_n
- hyper_stdtabsh sh == the hyperstandard tableau of shape sh : intpart,
that is the tableau obtained by filling the rows with consecutive
numbers, from bottom to top (in French conventions)
- conj_stdtabn t == the conjugate of t : stdtabn n in type stdtabn n
- conj_stdtabsh t == the conjugate of t : stdtabsh sh in type stdtabsh (conj_intpart sh)
- Lemma stdtab_of_yamP y : is_yam y -> is_stdtab (stdtab_of_yam y).
- Theorem stdtab_of_yamK y : is_yam y -> yam_of_stdtab (stdtab_of_yam y) = y.
- Lemma yam_of_stdtabP t : is_stdtab t -> is_yam (yam_of_stdtab t).
- Theorem yam_of_stdtabK t : is_stdtab t -> stdtab_of_yam (yam_of_stdtab t) = t.
- Lemma shape_stdtab_of_yam y : shape (stdtab_of_yam y) = evalseq y.
- Lemma shape_yam_of_stdtab t : is_stdtab t -> evalseq (yam_of_stdtab t) =
shape t.
- Lemma size_stdtab_of_yam y : size_tab (stdtab_of_yam y) = size y.
- Lemma size_yam_of_stdtab t : is_stdtab t -> size (yam_of_stdtab t) = size_tab
t.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup.
Require Import tools combclass partition Yamanouchi ordtype std tableau.
Set Implicit Arguments.
Import Order.Theory.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup.
Require Import tools combclass partition Yamanouchi ordtype std tableau.
Set Implicit Arguments.
Import Order.Theory.
Section AppendNth.
Variables (disp :unit) (T : inhOrderType disp).
Implicit Type b : T.
Implicit Type t : seq (seq T).
Definition append_nth t b i := set_nth [::] t i (rcons (nth [::] t i) b).
Lemma perm_append_nth t x pos :
perm_eq (to_word (append_nth t x pos)) (x :: to_word t).
Lemma shape_append_nth t b i : shape (append_nth t b i) = incr_nth (shape t) i.
Lemma size_append_nth t b i : size_tab (append_nth t b i) = (size_tab t).+1.
Lemma get_tab_append_nth (t : seq (seq T)) l i r c :
get_tab (append_nth t l i) (r, c) =
if (r == i) && (c == nth 0 (shape t) i) then l else get_tab t (r, c).
Variables (disp :unit) (T : inhOrderType disp).
Implicit Type b : T.
Implicit Type t : seq (seq T).
Definition append_nth t b i := set_nth [::] t i (rcons (nth [::] t i) b).
Lemma perm_append_nth t x pos :
perm_eq (to_word (append_nth t x pos)) (x :: to_word t).
Lemma shape_append_nth t b i : shape (append_nth t b i) = incr_nth (shape t) i.
Lemma size_append_nth t b i : size_tab (append_nth t b i) = (size_tab t).+1.
Lemma get_tab_append_nth (t : seq (seq T)) l i r c :
get_tab (append_nth t l i) (r, c) =
if (r == i) && (c == nth 0 (shape t) i) then l else get_tab t (r, c).
Fixpoint last_big t b :=
if t is t0 :: t' then
if last b t0 == b then 0
else (last_big t' b).+1
else 0.
Lemma allLeq_to_word_hd r t b : allLeq (to_word (r :: t)) b -> allLeq r b.
Lemma allLeq_to_word_tl r t b : allLeq (to_word (r :: t)) b -> allLeq (to_word t) b.
Lemma last_bigP t b i :
is_tableau t -> allLeq (to_word t) b ->
reflect (last b (nth [::] t i) = b /\
forall j, j < i -> (last b (nth [::] t j) < b)%O)
(i == last_big t b).
Lemma last_big_append_nth t b lb :
(forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) ->
last_big (append_nth t b lb) b = lb.
End AppendNth.
if t is t0 :: t' then
if last b t0 == b then 0
else (last_big t' b).+1
else 0.
Lemma allLeq_to_word_hd r t b : allLeq (to_word (r :: t)) b -> allLeq r b.
Lemma allLeq_to_word_tl r t b : allLeq (to_word (r :: t)) b -> allLeq (to_word t) b.
Lemma last_bigP t b i :
is_tableau t -> allLeq (to_word t) b ->
reflect (last b (nth [::] t i) = b /\
forall j, j < i -> (last b (nth [::] t j) < b)%O)
(i == last_big t b).
Lemma last_big_append_nth t b lb :
(forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) ->
last_big (append_nth t b lb) b = lb.
End AppendNth.
Section Bijection.
Implicit Type y : seq nat.
Implicit Types t : seq (seq nat).
Definition is_stdtab t := is_tableau t && is_std (to_word t).
Lemma stdtabP t : is_stdtab t -> is_tableau t.
Fixpoint stdtab_of_yam y :=
if y is y0 :: y' then
append_nth (stdtab_of_yam y') (size y') y0
else [::].
Lemma shape_stdtab_of_yam y : shape (stdtab_of_yam y) = evalseq y.
Lemma size_stdtab_of_yam y : size_tab (stdtab_of_yam y) = size y.
Lemma std_of_yam y : is_std (to_word (stdtab_of_yam y)).
Implicit Type y : seq nat.
Implicit Types t : seq (seq nat).
Definition is_stdtab t := is_tableau t && is_std (to_word t).
Lemma stdtabP t : is_stdtab t -> is_tableau t.
Fixpoint stdtab_of_yam y :=
if y is y0 :: y' then
append_nth (stdtab_of_yam y') (size y') y0
else [::].
Lemma shape_stdtab_of_yam y : shape (stdtab_of_yam y) = evalseq y.
Lemma size_stdtab_of_yam y : size_tab (stdtab_of_yam y) = size y.
Lemma std_of_yam y : is_std (to_word (stdtab_of_yam y)).
The following proof is an experiment to see if proof using get_tab are
easier than proof by induction on the structure of tableaux
Lemma is_tab_append_nth_size_alternative_proof r T n :
all (gtn n) (to_word T) ->
is_part (incr_nth (shape T) r) ->
is_tableau T -> is_tableau (append_nth T n r).
Lemma is_tab_append_nth_size r T n :
all (gtn n) (to_word T) ->
is_part (incr_nth (shape T) r) ->
is_tableau T -> is_tableau (append_nth T n r).
Lemma stdtab_of_yamP y : is_yam y -> is_stdtab (stdtab_of_yam y).
Section StdTabInd.
Fixpoint remn_rec t n :=
if t is t0 :: t' then
match t0 with
| [::] => [::]
| l0 :: t0' => if last l0 t0' == n then
if t0' == [::] then [::]
else (belast l0 t0') :: t'
else t0 :: remn_rec t' n
end
else [::] .
Definition remn t := remn_rec t (size_tab t).-1.
Lemma remnP t :
is_stdtab t -> t != [::] ->
is_tableau (remn t) /\
append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
Lemma is_stdtab_remn t : is_stdtab t -> is_stdtab (remn t).
Lemma append_nth_remn t :
is_stdtab t -> t != [::] ->
append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
Lemma size_tab_remn t :
is_stdtab t -> t != [::] -> size_tab (remn t) = (size_tab t).-1.
End StdTabInd.
Fixpoint yam_of_stdtab_rec n t :=
if n is n'.+1 then
(last_big t n') :: yam_of_stdtab_rec n' (remn t)
else [::].
Definition yam_of_stdtab t := yam_of_stdtab_rec (size_tab t) t.
Lemma size_yam_of_stdtab_rec n t : size (yam_of_stdtab_rec n t) = n.
Theorem yam_of_stdtabK t : is_stdtab t -> stdtab_of_yam (yam_of_stdtab t) = t.
Lemma find_append_nth (l : nat) t r :
l \notin (to_word t) ->
find (fun x : seq nat => l \in x) (append_nth t l r) = r.
Lemma size_notin_stdtab_of_yam y : (size y) \notin (to_word (stdtab_of_yam y)).
Lemma incr_nth_injl u v i :
0 \notin u -> 0 \notin v -> incr_nth u i = incr_nth v i -> u = v.
Lemma shape0 d (T : orderType d) (u : seq (seq T)) :
[::] \notin u -> 0 \notin (shape u).
Lemma append_nth_injl d (T : inhOrderType d) (u v : seq (seq T)) (l : T) p :
[::] \notin u -> [::] \notin v ->
append_nth u l p = append_nth v l p -> u = v.
Lemma stdtab_of_yam_nil y : is_yam y -> [::] \notin (stdtab_of_yam y).
Lemma stdtab_of_yam_inj x y :
is_yam x -> is_yam y -> stdtab_of_yam x = stdtab_of_yam y -> x = y.
Lemma shape_yam_of_stdtab t :
is_stdtab t -> evalseq (yam_of_stdtab t) = shape t.
Lemma size_yam_of_stdtab t :
is_stdtab t -> size (yam_of_stdtab t) = size_tab t.
Lemma part_yam_of_stdtab t :
is_stdtab t -> is_part (evalseq (yam_of_stdtab t)).
Lemma yam_of_stdtabP t : is_stdtab t -> is_yam (yam_of_stdtab t).
Theorem stdtab_of_yamK y : is_yam y -> yam_of_stdtab (stdtab_of_yam y) = y.
End Bijection.
Lemma eq_inv_is_row (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
eq_inv u1 u2 -> is_row u1 -> is_row u2.
Lemma is_row_stdE (d : unit) (T : inhOrderType d) (w : seq T) :
is_row (std w) = is_row w.
all (gtn n) (to_word T) ->
is_part (incr_nth (shape T) r) ->
is_tableau T -> is_tableau (append_nth T n r).
Lemma is_tab_append_nth_size r T n :
all (gtn n) (to_word T) ->
is_part (incr_nth (shape T) r) ->
is_tableau T -> is_tableau (append_nth T n r).
Lemma stdtab_of_yamP y : is_yam y -> is_stdtab (stdtab_of_yam y).
Section StdTabInd.
Fixpoint remn_rec t n :=
if t is t0 :: t' then
match t0 with
| [::] => [::]
| l0 :: t0' => if last l0 t0' == n then
if t0' == [::] then [::]
else (belast l0 t0') :: t'
else t0 :: remn_rec t' n
end
else [::] .
Definition remn t := remn_rec t (size_tab t).-1.
Lemma remnP t :
is_stdtab t -> t != [::] ->
is_tableau (remn t) /\
append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
Lemma is_stdtab_remn t : is_stdtab t -> is_stdtab (remn t).
Lemma append_nth_remn t :
is_stdtab t -> t != [::] ->
append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
Lemma size_tab_remn t :
is_stdtab t -> t != [::] -> size_tab (remn t) = (size_tab t).-1.
End StdTabInd.
Fixpoint yam_of_stdtab_rec n t :=
if n is n'.+1 then
(last_big t n') :: yam_of_stdtab_rec n' (remn t)
else [::].
Definition yam_of_stdtab t := yam_of_stdtab_rec (size_tab t) t.
Lemma size_yam_of_stdtab_rec n t : size (yam_of_stdtab_rec n t) = n.
Theorem yam_of_stdtabK t : is_stdtab t -> stdtab_of_yam (yam_of_stdtab t) = t.
Lemma find_append_nth (l : nat) t r :
l \notin (to_word t) ->
find (fun x : seq nat => l \in x) (append_nth t l r) = r.
Lemma size_notin_stdtab_of_yam y : (size y) \notin (to_word (stdtab_of_yam y)).
Lemma incr_nth_injl u v i :
0 \notin u -> 0 \notin v -> incr_nth u i = incr_nth v i -> u = v.
Lemma shape0 d (T : orderType d) (u : seq (seq T)) :
[::] \notin u -> 0 \notin (shape u).
Lemma append_nth_injl d (T : inhOrderType d) (u v : seq (seq T)) (l : T) p :
[::] \notin u -> [::] \notin v ->
append_nth u l p = append_nth v l p -> u = v.
Lemma stdtab_of_yam_nil y : is_yam y -> [::] \notin (stdtab_of_yam y).
Lemma stdtab_of_yam_inj x y :
is_yam x -> is_yam y -> stdtab_of_yam x = stdtab_of_yam y -> x = y.
Lemma shape_yam_of_stdtab t :
is_stdtab t -> evalseq (yam_of_stdtab t) = shape t.
Lemma size_yam_of_stdtab t :
is_stdtab t -> size (yam_of_stdtab t) = size_tab t.
Lemma part_yam_of_stdtab t :
is_stdtab t -> is_part (evalseq (yam_of_stdtab t)).
Lemma yam_of_stdtabP t : is_stdtab t -> is_yam (yam_of_stdtab t).
Theorem stdtab_of_yamK y : is_yam y -> yam_of_stdtab (stdtab_of_yam y) = y.
End Bijection.
Lemma eq_inv_is_row (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
(u1 : seq T1) (u2 : seq T2) :
eq_inv u1 u2 -> is_row u1 -> is_row u2.
Lemma is_row_stdE (d : unit) (T : inhOrderType d) (w : seq T) :
is_row (std w) = is_row w.
Section StdtabOfShape.
Definition is_stdtab_of_shape sh := [pred t | (is_stdtab t) && (shape t == sh) ].
Definition enum_stdtabsh sh : seq (seq (seq nat)) :=
map stdtab_of_yam (enum_yameval sh).
Variable sh : intpart.
Structure stdtabsh : Set :=
StdtabSh {
stdtabshval :> seq (seq nat);
_ : is_stdtab_of_shape sh stdtabshval
}.
Let stdtabsh_enum : seq stdtabsh := pmap insub (enum_stdtabsh sh).
Fact finite_stdtabsh : Finite.axiom stdtabsh_enum.
Lemma stdtabshP (t : stdtabsh) : is_stdtab t.
Lemma shape_stdtabsh (t : stdtabsh) : shape t = sh.
Lemma enum_stdtabshE : map val (enum {:stdtabsh}) = enum_stdtabsh sh.
Fact hyper_stdtabsh_subproof :
is_stdtab_of_shape sh (stdtab_of_yam (locked (hyper_yameval sh))).
Definition hyper_stdtabsh := StdtabSh hyper_stdtabsh_subproof.
End StdtabOfShape.
#[export] Hint Resolve stdtabshP : core.
Section StdtabCombClass.
Variable n : nat.
Definition is_stdtab_of_n := [pred t | (is_stdtab t) && (size_tab t == n) ].
Structure stdtabn : Set :=
StdtabN {stdtabnval :> seq (seq nat); _ : is_stdtab_of_n stdtabnval}.
Definition enum_stdtabn : seq (seq (seq nat)) :=
map (stdtab_of_yam \o val) (enum ({:yamn n})).
Let stdtabn_enum : seq stdtabn := pmap insub enum_stdtabn.
Fact finite_stdtabn : Finite.axiom stdtabn_enum.
Lemma stdtabnP (s : stdtabn) : is_stdtab s.
Lemma size_tab_stdtabn (s : stdtabn) : size_tab s = n.
Lemma sumn_shape_stdtabnE (Q : stdtabn) : (sumn (shape Q)) = n.
Lemma is_part_shape_deg (Q : stdtabn) : is_part_of_n n (shape Q).
Definition shape_deg (Q : stdtabn) := IntPartN (is_part_shape_deg Q).
End StdtabCombClass.
Section StdtabnOfStdtabsh.
Variables (n : nat) (sh : intpartn n).
Fact stdtabn_of_sh_subproof (t : stdtabsh sh) : is_stdtab_of_n n t.
Definition stdtabn_of_sh t := StdtabN (stdtabn_of_sh_subproof t).
Lemma shape_deg_stdtabn_of_sh t :
shape_deg (stdtabn_of_sh t) = sh.
End StdtabnOfStdtabsh.
Definition is_stdtab_of_shape sh := [pred t | (is_stdtab t) && (shape t == sh) ].
Definition enum_stdtabsh sh : seq (seq (seq nat)) :=
map stdtab_of_yam (enum_yameval sh).
Variable sh : intpart.
Structure stdtabsh : Set :=
StdtabSh {
stdtabshval :> seq (seq nat);
_ : is_stdtab_of_shape sh stdtabshval
}.
Let stdtabsh_enum : seq stdtabsh := pmap insub (enum_stdtabsh sh).
Fact finite_stdtabsh : Finite.axiom stdtabsh_enum.
Lemma stdtabshP (t : stdtabsh) : is_stdtab t.
Lemma shape_stdtabsh (t : stdtabsh) : shape t = sh.
Lemma enum_stdtabshE : map val (enum {:stdtabsh}) = enum_stdtabsh sh.
Fact hyper_stdtabsh_subproof :
is_stdtab_of_shape sh (stdtab_of_yam (locked (hyper_yameval sh))).
Definition hyper_stdtabsh := StdtabSh hyper_stdtabsh_subproof.
End StdtabOfShape.
#[export] Hint Resolve stdtabshP : core.
Section StdtabCombClass.
Variable n : nat.
Definition is_stdtab_of_n := [pred t | (is_stdtab t) && (size_tab t == n) ].
Structure stdtabn : Set :=
StdtabN {stdtabnval :> seq (seq nat); _ : is_stdtab_of_n stdtabnval}.
Definition enum_stdtabn : seq (seq (seq nat)) :=
map (stdtab_of_yam \o val) (enum ({:yamn n})).
Let stdtabn_enum : seq stdtabn := pmap insub enum_stdtabn.
Fact finite_stdtabn : Finite.axiom stdtabn_enum.
Lemma stdtabnP (s : stdtabn) : is_stdtab s.
Lemma size_tab_stdtabn (s : stdtabn) : size_tab s = n.
Lemma sumn_shape_stdtabnE (Q : stdtabn) : (sumn (shape Q)) = n.
Lemma is_part_shape_deg (Q : stdtabn) : is_part_of_n n (shape Q).
Definition shape_deg (Q : stdtabn) := IntPartN (is_part_shape_deg Q).
End StdtabCombClass.
Section StdtabnOfStdtabsh.
Variables (n : nat) (sh : intpartn n).
Fact stdtabn_of_sh_subproof (t : stdtabsh sh) : is_stdtab_of_n n t.
Definition stdtabn_of_sh t := StdtabN (stdtabn_of_sh_subproof t).
Lemma shape_deg_stdtabn_of_sh t :
shape_deg (stdtabn_of_sh t) = sh.
End StdtabnOfStdtabsh.
Section ConjTab.
Variables (disp: unit) (T : inhOrderType disp).
Definition conj_tab (t : seq (seq T)) : seq (seq T) :=
let c := conj_part (shape t) in
mkseq (fun i => mkseq (fun j => get_tab t (j, i)) (nth 0 c i)) (size c).
Lemma size_conj_tab t : size (conj_tab t) = size (conj_part (shape t)).
Lemma shape_conj_tab t : shape (conj_tab t) = conj_part (shape t).
Lemma get_conj_tab t :
is_part (shape t) ->
forall i j, get_tab (conj_tab t) (i, j) = get_tab t (j, i).
Lemma eq_from_shape_get_tab (t u : seq (seq T)) :
shape t = shape u -> get_tab t =1 get_tab u -> t = u.
Lemma conj_tab_shapeK t : is_part (shape t) -> conj_tab (conj_tab t) = t.
Lemma conj_tabK t : is_tableau t -> conj_tab (conj_tab t) = t.
Lemma append_nth_conj_tab (t : seq (seq T)) l i :
is_part (shape t) ->
is_add_corner (shape t) i ->
conj_tab (append_nth t l i) = append_nth (conj_tab t) l (nth 0 (shape t) i).
End ConjTab.
Example conj_tab_expl1 :
conj_tab [:: [:: 0; 1; 4]; [:: 2; 3]] ==
[:: [:: 0; 2]; [:: 1; 3]; [:: 4]].
Example conj_tab_expl2 :
conj_tab [:: [:: 0; 1; 3; 4]; [:: 2; 5]; [:: 6]] ==
[:: [:: 0; 2; 6]; [:: 1; 5]; [:: 3]; [:: 4]].
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.
Lemma is_stdtab_conj t : is_stdtab t -> is_stdtab (conj_tab t).
Lemma conj_stdtabnP n (t : stdtabn n):
is_stdtab_of_n n (conj_tab t).
Canonical conj_stdtabn n (t : stdtabn n) := StdtabN (conj_stdtabnP t).
Lemma conj_stdtabshP (sh : intpart) (t : stdtabsh sh) :
is_stdtab_of_shape (conj_part sh) (conj_tab t).
Canonical conj_stdtabsh {sh : intpart} (t : stdtabsh sh) :=
StdtabSh (conj_stdtabshP t).
Definition stdtabshcast m n (eq_mn : m = n) t :=
let: erefl in _ = n := eq_mn return stdtabsh n in t.
Lemma val_stdtabshcast m n (eq_mn : m = n) t :
val (stdtabshcast eq_mn t) = val t.
Lemma conj_stdtabsh_bij sh : bijective (@conj_stdtabsh sh).
Lemma card_stdtabsh_conj_part (sh : intpart) :
#|{:stdtabsh (conj_part sh)}| = #|{:stdtabsh sh}|.
#[export] Hint Resolve stdtabnP stdtabshP : core.
Variables (disp: unit) (T : inhOrderType disp).
Definition conj_tab (t : seq (seq T)) : seq (seq T) :=
let c := conj_part (shape t) in
mkseq (fun i => mkseq (fun j => get_tab t (j, i)) (nth 0 c i)) (size c).
Lemma size_conj_tab t : size (conj_tab t) = size (conj_part (shape t)).
Lemma shape_conj_tab t : shape (conj_tab t) = conj_part (shape t).
Lemma get_conj_tab t :
is_part (shape t) ->
forall i j, get_tab (conj_tab t) (i, j) = get_tab t (j, i).
Lemma eq_from_shape_get_tab (t u : seq (seq T)) :
shape t = shape u -> get_tab t =1 get_tab u -> t = u.
Lemma conj_tab_shapeK t : is_part (shape t) -> conj_tab (conj_tab t) = t.
Lemma conj_tabK t : is_tableau t -> conj_tab (conj_tab t) = t.
Lemma append_nth_conj_tab (t : seq (seq T)) l i :
is_part (shape t) ->
is_add_corner (shape t) i ->
conj_tab (append_nth t l i) = append_nth (conj_tab t) l (nth 0 (shape t) i).
End ConjTab.
Example conj_tab_expl1 :
conj_tab [:: [:: 0; 1; 4]; [:: 2; 3]] ==
[:: [:: 0; 2]; [:: 1; 3]; [:: 4]].
Example conj_tab_expl2 :
conj_tab [:: [:: 0; 1; 3; 4]; [:: 2; 5]; [:: 6]] ==
[:: [:: 0; 2; 6]; [:: 1; 5]; [:: 3]; [:: 4]].
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.
Lemma is_stdtab_conj t : is_stdtab t -> is_stdtab (conj_tab t).
Lemma conj_stdtabnP n (t : stdtabn n):
is_stdtab_of_n n (conj_tab t).
Canonical conj_stdtabn n (t : stdtabn n) := StdtabN (conj_stdtabnP t).
Lemma conj_stdtabshP (sh : intpart) (t : stdtabsh sh) :
is_stdtab_of_shape (conj_part sh) (conj_tab t).
Canonical conj_stdtabsh {sh : intpart} (t : stdtabsh sh) :=
StdtabSh (conj_stdtabshP t).
Definition stdtabshcast m n (eq_mn : m = n) t :=
let: erefl in _ = n := eq_mn return stdtabsh n in t.
Lemma val_stdtabshcast m n (eq_mn : m = n) t :
val (stdtabshcast eq_mn t) = val t.
Lemma conj_stdtabsh_bij sh : bijective (@conj_stdtabsh sh).
Lemma card_stdtabsh_conj_part (sh : intpart) :
#|{:stdtabsh (conj_part sh)}| = #|{:stdtabsh sh}|.
#[export] Hint Resolve stdtabnP stdtabshP : core.