proposition: Lemma mg_minimal (L : dlang char) (M : mgClassifier L) : minimal (mg_to_dfa M).
proof: Proof. apply/minimalP. split; first exact: mg_to_connected. move => p q. split => [coll_pq|->//]. rewrite -[p](crK (Sf := (@imfun_of_surj _ M))). rewrite -[q](crK (Sf := (@imfun_of_surj _ M))). apply: val_inj. apply/nerodeP => w. rewrite -!(@classifier_to_dfa_correct _ M) !inE /dfa_accept !delta_cat. rewrite -!/(delta_s _ _) !classifier_to_dfa_delta !crK. exact: coll_pq. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)