proposition: Lemma compareList_eq_axiom : forall l1 l2, compareList l1 l2 = Eq <-> l1 = l2.
proof: Proof. elim => [ | hd tl hi] [ | hd' tl'] //= ; split. - have := (@compare_eq_axiom hd hd'). case: (compare hd hd') => //=. move => -> //=. case: (hi tl') => hhi _. move => h; by rewrite (hhi h). - case => -> ->. by rewrite compare_refl compareList_refl. 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)