proposition: Lemma prune_eq_connected : #|A| = #|dfa_prune| -> connected A.
proof: Proof. move => H. apply/connectedP. apply/forallP => x. by move: (cardT_eq (Logic.eq_sym H)) ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)