proposition: Lemma all_ltn_nth_tabsh t (i : nat) : all (fun x : 'I_n.+1 => (i <= x)%O) (nth [::] t i).
proof: Proof. have:= tabshP t => /is_tableauP[_ _ Hdom]. elim: i => [|i /allP IHi]; apply/allP => x //. move/(_ _ _ (ltnSn i)): Hdom => /dominateP[Hsz]; move: inh => Z. move: (nth [::] t i) (nth [::] t i.+1) Hsz IHi => Ri Ri1 Hsz IHi Hdom Hx. have:= Hx; rewrite -index_mem => Hxind. have:= Hxind => /leq_trans/(_ Hsz)/(mem_nth Z){}/IHi/leq_ltn_trans; apply. by move/(_ _ Hxind): Hdom; rewrite nth_index. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted