proposition: Lemma tabwordshape_col d (w : d.-tuple 'I_n) : tabsh_reading (colpartn d) w = sorted >%O w.
proof: Proof. Proof using. rewrite /tabsh_reading /= colpartnE ; case: w => w /=/eqP Hw. have -> : sumn (nseq d 1%N) = d. by elim: d {Hw} => //= d /= ->; rewrite add1n. rewrite Hw eq_refl /= rev_nseq. have -> : rev (reshape (nseq d 1%N) w) = [seq [:: i] | i <- rev w]. rewrite map_rev; congr rev. elim: d w Hw => [| d IHd] //=; first by case. case => [| w0 w] //= /eqP; rewrite eqSS => /eqP /IHd <-. by rewrite take0 drop0. rewrite -rev_sorted. case: {w} (rev w) {d Hw} => [|w0 w] //=. elim: w w0 => [//= | w1 w /= <-] w0 /=. by congr andb; rewrite /dominate /= andbT {w}. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau