proposition: Theorem dfa2_to_dfa : { A : dfa char | dfa_lang A =i dfa2_lang M & #|A| <= (#|M|.+1)^(#|M|.+1) }.
proof: Proof. exists (classifier_to_dfa (dfa2_to_myhill)); first exact: classifier_to_dfa_correct. rewrite card_sub (leqRW (max_card _)). exact: det_range. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)