proposition: Lemma dfa_compl_correct w : w \in dfa_lang dfa_compl = (w \notin dfa_lang A1).
proof: Proof. rewrite /dfa_lang !inE {2}/dfa_compl /=. by rewrite /dfa_accept inE. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)