proposition: Lemma minimalP A : minimal A <-> (connected A /\ collapsed A).
proof: Proof. split. - move => H. split. exact: minimal_connected. exact: minimal_collapsed. - move => [H1 H2] B L_AB. apply: leq_trans _ (minimize_size _). apply: eq_leq. apply: dfa_iso_size. apply: coll_iso => // x. by rewrite minimize_correct. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)