proposition: Lemma wder_Atom : forall u n, wder u (Atom n) = Atom n \/ wder u (Atom n) = Eps \/ wder u (Atom n) = Void.
proof: Proof. case => [ | hd ] /=. move => n; by left. case => [ | hd' tl'] n /=. case : eq_op. by right; left. by right; right. case: eq_op => /=; by right;right; rewrite wder_Void. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)