proposition: Lemma is_comp_cat s1 s2 : is_comp (s1 ++ s2) = (is_comp s1) && (is_comp s2).
proof: Proof. by rewrite /is_comp mem_cat negb_or. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype