proposition: Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|.
proof: Proof. move => [iso [H _ _ _]]. exact (bij_eq_card H). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)