proposition: Lemma regular_quotL (char: finType) (L1 L2 : lang char) : regular L1 -> regular L2 -> regular (quotL L1 L2).
proof: Proof. move => [A acc_L1] [B acc_L2]. apply: regular_quotL_aux acc_L2 _ => q. pose B_q := {| dfa_s := dfa_s B; dfa_fin := [set q] ; dfa_trans := @dfa_trans _ B |}. have B_qP y : delta_s B y = q <-> y \in dfa_lang B_q. { rewrite -delta_lang inE. by split => ?; exact/eqP. } pose dec := dfa_inhab (dfa_op andb A B_q). apply: dec_iff dec _. split. - move => [y] H1 Hq. exists y. rewrite dfa_op_correct. apply/andP;split; first exact/acc_L1. exact/B_qP. - move => [y]. rewrite dfa_op_correct => /andP [H1 H2]. exists y; first exact/acc_L1. exact/B_qP. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)