proposition: Lemma dfa_to_re_size : re_size dfa_to_re <= (#|A| * (c * 4 ^ (2 * #|A|)).+1).+1.
proof: Proof. rewrite /dfa_to_re -big_filter (leqRW (big_plus_size (m := R_size_rec #|A|)_)). - rewrite -(leqRW (R_size_high _)) size_filter (leqRW (count_size _ _)). by rewrite ltnS /index_enum -enumT cardE. - move => q _. exact: R_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)