proposition: Lemma is_tableau_catl t1 t2 : is_tableau (t1 ++ t2) -> is_tableau t1.
proof: Proof. elim: t1 => [// | t t1 IHt1] /= /and4P[-> -> /= Hdom {}/IHt1->]. by rewrite andbT; case: t1 Hdom => [// | r1 t1]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted