proposition: Lemma regular_rev (char : finType) (L : lang char) : regular L -> regular (fun x => L (rev x)).
proof: Proof. case/regularP => e H. apply/regularP. exists (Rev e) => x. by rewrite Rev_correct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)