proposition: Lemma compare_neg : forall c1 c2, compare c2 c1 = CompOpp (compare c1 c2).
proof: Proof. apply (@creg_ind (fun c1 => forall c2 , compare c2 c1 = CompOpp (compare c1 c2)) (fun l1 => forall l2, compareList l2 l1 = CompOpp (compareList l1 l2))) => [ | | | s | c hc | l hl | l hl | l hl | c hc | | hd hc tl htl ] /=; try (by case => /=). - case => //= s'. by apply : cmpS_neg. - case => [ | hd' tl'] //=. move: (hc hd'). case: (compare hd' hd) => h //=. by rewrite (comparison_negK h) /=. by rewrite (comparison_negK h) /=. by rewrite (comparison_negK h) /=. 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)