fact: Definition cmpb (a b: bool) : comparison := match a,b with | true,true => Eq | true,false => Gt | false,false => Eq | false,true => Lt end.
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)