fact: Fixpoint deprecated_string_cmp (l r : string) : comparison := match l , r with | EmptyString , EmptyString => Eq | EmptyString , _ => Lt | _ , EmptyString => Gt | String l ls , String r rs => ascii_cmp l r >> deprecated_string_cmp ls rs end.
imports: Coq.Strings.String Coq.Program.Program Coq.Arith.PeanoNat ExtLib.Tactics.Consider ExtLib.Core.RelDec ExtLib.Structures.Reducible ExtLib.Structures.Monoid ExtLib.Data.Char ExtLib.Data.Nat