proposition: Lemma classifier_to_dfa_connected L (M : classifier_for L) : connected (classifier_to_dfa M).
proof: Proof. move => q. exists (cr (@imfun_of_surj _ M) q). rewrite -{2}[q](crK (Sf:=(@imfun_of_surj _ M))). by rewrite -/(delta_s _ _) classifier_to_dfa_delta. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)