fact: Fixpoint string_compare str1 str2 := match str1, str2 with | EmptyString, EmptyString => Eq | EmptyString, _ => Lt | _, EmptyString => Gt | String char1 tail1, String char2 tail2 => match Nat.compare (nat_of_ascii char1) (nat_of_ascii char2) with | Eq => string_compare tail1 tail2 | Lt => Lt | Gt => Gt end end.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat