proposition: Lemma size_tabsh t : size t <= n.+1.
proof: Proof. have Hall := all_ltn_nth_tabsh t. have:= tabshP t => /is_tableauP[Hnnil _ _]. apply contraT; rewrite -ltnNge => Hn. move/(_ n.+1): Hall; move/(_ _ Hn): Hnnil => {Hn}. case: (nth [::] t n.+1) => //= x s _ /andP[Hn _ {s}]. have:= ltn_ord x; rewrite ltnS => /(leq_trans Hn). by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted