proposition: Lemma dfa_to_re_correct : dfa_lang A =i dfa_to_re.
proof: Proof. move => w. apply/idP/big_plusP => [H|[x Hx]]. - exists (delta_s A w) => //. by rewrite -L_R set_enum dfa_L. - by rewrite -L_R set_enum dfa_L inE /dfa_accept => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)