proposition: Lemma wder_rcons : forall a u (r:bregexp), wder (rcons u a) r = der a (wder u r).
proof: Proof. move => a. elim => [ | hd tl hi] //= r. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)