proposition: Lemma mg_eq_proof L1 L2 (N1 : mgClassifier L1) : L1 =i L2 -> nerode L2 N1.
proof: Proof. move => H0 u v. split => [/nerodeP H1 w|H1]. - by rewrite -!H0. - apply/nerodeP => w. by rewrite !H0. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)