fact: Fixpoint compare (s1 s2 : string) : comparison := match s1, s2 with | EmptyString, EmptyString => Eq | EmptyString, String _ _ => Lt | String _ _ , EmptyString => Gt | String c1 s1', String c2 s2' => match Ascii.compare c1 c2 with | Eq => compare s1' s2' | ne => ne end end.
imports: Arith Ascii Bool Coq.Strings.Byte