proposition: Lemma in_der_compat : forall (r1 r2:bregexp) , r1 ≡ r2 -> forall a,(der a r1) ≡ (der a r2).
proof: Proof. move => r1 r2 heq a u. by rewrite !derE !in_residual !heq. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)