proposition: Lemma nfa_regular L : regular L <-T-> { N : nfa | forall x, L x <-> x \in nfa_lang N }.
proof: Proof. split => [[A]|[N]] H. exists (dfa_to_nfa A) => x. by rewrite -dfa_to_nfa_correct. exists (nfa_to_dfa N) => x. by rewrite -nfa_to_dfa_correct. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)