proposition: Lemma tab0 t : is_tableau t -> size_tab t = 0 -> t = [::].
proof: Proof. Proof using. move/is_part_sht; rewrite /size_tab => /part0 /[apply]. by rewrite /shape; case t. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted