proposition: Lemma compareList_trans : forall l1 l2 l3 s, compareList l1 l2 = s -> compareList l2 l3 = s -> compareList l1 l3 = s.
proof: Proof. elim => [ | hd tl hi] => //=. - case => [ | hd' tl'] //=. - case => [ | hd'' tl''] //=. by move => s <-. - case => [ | hd' tl' ] //=. case => [ | hd'' tl''] //= ; by move => s <-. case => [ | hd'' tl''] //=. move => s. move: (@compare_trans hd hd' hd'' s). move: (hi tl' tl'' s); clear hi. case_eq (compare hd hd') => h1 //=. * rewrite (compare_eq_axiom h1); by case: (compare hd' hd''). * case_eq (compare hd' hd'') => h2 //=. rewrite -(compare_eq_axiom h2) h1. by move => _ _ <- _. move => _ h hs _. move : h; rewrite -hs. by move => ->. by move => _ _ <-. * case_eq (compare hd' hd'') => h2 //=. rewrite -(compare_eq_axiom h2) h1. by move => _ _ <- _. by move => _ _ <-. move => _ h hs _. move : h; rewrite -hs. by move => ->. 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)