proposition: Lemma Neg_correct (char : finType) (r : regexp char) w : w \in Neg r = (w \notin r).
proof: Proof. by rewrite /Neg -dfa_to_re_correct dfa_compl_correct !re_to_dfa_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)