proposition: Lemma shape0 d (T : orderType d) (u : seq (seq T)) : [::] \notin u -> 0 \notin (shape u).
proof: Proof. apply: contra; rewrite /shape; elim: u => [//=| u0 u IHu] /=. rewrite !inE => /orP[]. - by rewrite eq_sym => /nilP ->. - by move/IHu ->; rewrite orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau