proposition: Lemma minimal_connected A : minimal A -> connected A.
proof: Proof. move => MA. apply: prune_eq_connected. apply/eqP. rewrite eqn_leq dfa_prune_size andbT. apply: MA => x. by rewrite dfa_prune_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)