proposition: Lemma is_tableau_rconsK t (tn : seq T) : is_tableau (rcons t tn) -> is_tableau t.
proof: Proof. Proof using. elim: t => [// | t0 t IHt] /= /and4P[-> -> Hdom {}/IHt->] /=. by case: t Hdom => [// | t1 t]; rewrite rcons_cons /= => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted