proposition: Lemma compare_refl : forall r, compare r r = Eq.
proof: Proof. apply creg_ind with (fun l => compareList l l = Eq) => //=. - apply cmpS_refl. - by move => c1 -> c2 ->. 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)