proposition: Lemma minimize_size (A : dfa) : #|minimize A| <= #|A|.
proof: Proof. exact: leq_trans (collapse_size _) (dfa_prune_size _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)