proposition: Lemma bregexp_dec : forall (r1 r2:bregexp), {r1 ≡ r2}+{~ r1 ≡ r2}.
proof: Proof. move => r1 r2. have:= bregexp_eqP r1 r2. case : (bregexp_eq r1 r2). move => h. left. by apply/h. move => h. right. by move/h. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)