proposition: Lemma regular_inter (L1 L2 : lang char) : regular L1 -> regular L2 -> regular (fun x => L1 x /\ L2 x).
proof: Proof. move => [A LA] [B LB]. exists (dfa_op andb A B) => x. by rewrite dfa_op_correct LA LB (rwP andP). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)