proposition: Lemma tabwordshape_row d (w : d.-tuple 'I_n) : tabsh_reading (rowpartn d) w = sorted leq [seq val i | i <- w].
proof: Proof. Proof using. rewrite /tabsh_reading /= rowpartnE ; case: w => w /=/eqP Hw. case: d Hw => [//= | d] Hw; rewrite Hw /=; first by case: w Hw. rewrite addn0 eq_refl andbT //=. case: w Hw => [//= | w0 w] /= /eqP; rewrite eqSS => /eqP <-. rewrite take_size; apply esym; apply (map_path (b := pred0)) => //. by apply/hasPn => x /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau