proposition: Lemma minimize_connected (A : dfa) : connected (minimize A).
proof: Proof. apply collapse_connected. exact: dfa_prune_connected. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)