proposition: Lemma minimal_nerode : nerode (dfa_lang A) (delta_s A).
proof: Proof. Proof using MA. move => u v. apply: iff_trans (iff_sym (minimal_collapsed MA _ _)) _. by split => H w; move: (H w); rewrite -!delta_cat !delta_lang. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)