proposition: Lemma A_start_cat x y : (x ++ y \in dfa_lang A) = (y \in dfa_lang (A_start (delta_s A x))).
proof: Proof. rewrite inE /delta_s. elim: x (dfa_s A)=> //= a x IH q. by rewrite accE IH. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)