proposition: Lemma re_to_dfa_size e : #|re_to_dfa e| <= 2^(2 * re_size e).
proof: Proof. by rewrite card_set leq_pexp2l // re_to_nfa_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)