proposition: Lemma minimal_collapsed A : minimal A -> collapsed A.
proof: Proof. move => MA. have B : bijective (\pi_(collapse_state A)). apply: surj_card_bij. - move => x. exists (repr x). by rewrite reprK. - apply/eqP. rewrite eqn_leq collapse_size (MA (collapse A)) // => x. by rewrite collapse_correct. move => x y. split => [|->]; last exact/collP/collb_refl. move/collP/eqmodP. exact: bij_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)