proposition: Lemma is_part_sht t : is_tableau t -> is_part (shape t).
proof: Proof. Proof using. elim: t => [// | t0 t IHt] /= /and4P[Ht0 _ /dominateP[Hdom _ Htab]]. rewrite (IHt Htab) andbT {IHt Htab} /shape. by case: t Hdom => //=; case: t0 Ht0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted