proposition: Lemma cmpb_eq_axiom : forall a b, reflect (a=b) (cmpb a b == Eq).
proof: Proof. move => a b; apply: (iffP idP). by case: a b => [] []. move => -> /=. by case: b. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)