proposition: Lemma regular_quotR (char : finType) (L1 L2 : lang char) : regular L1 -> regular L2 -> regular (quotR L1 L2).
proof: Proof. move => [A LA] reg2. suff dec_L1 q : decidable (exists2 y, L2 y & delta q y \in dfa_fin A). { exists (dfa_quot dec_L1) => x. apply: (rwP (dfa_quotP _ _ _)) => {} x. by rewrite LA. } case: reg2 => {LA} [B LB]. pose C := {| dfa_s := q ; dfa_fin := dfa_fin A ; dfa_trans := @dfa_trans _ A |}. pose dec := dfa_inhab (dfa_op andb B C). apply: (dec_iff dec); split. - move => [x X1 X2]. exists x. rewrite dfa_op_correct. apply/andP;split => //. exact/LB. - move => [x]. rewrite dfa_op_correct. case/andP => *. exists x => //. exact/LB. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)