proposition: Lemma tabsh_readingP (sh : seq nat) (w : seq A) : reflect (exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w]) (tabsh_reading sh w).
proof: Proof. Proof using. apply (iffP idP). - move=> /andP[/eqP Hsz Htab]. exists (rev (reshape (rev sh) w)); split => //. + rewrite shape_rev -{2}(revK sh); congr (rev _). by apply: reshapeKl; rewrite sumn_rev Hsz. + by rewrite /to_word revK; apply: reshapeKr; rewrite sumn_rev Hsz. - move=> [] tab [] Htab Hsh Hw; apply/andP; split. + by rewrite -Hw size_to_word /size_tab Hsh. + rewrite -Hw /to_word -Hsh. by rewrite /shape -map_rev -/(shape _) flattenK revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted