[Agda] fast DecTotalOrder

[Sergei Meshveliani]

Can people, please, advise me on the following matter?
(which is in fact on Standard library)

For testing the sorting function for performance, I need 
(1) the list elements to be from some DecTotalOrder instance
     (required by the `sort' function),
(2) _≤?_ to perform fast,
(3) forming a list having as many different elements as needed.

I am going to do this.

a) To implement  
   stoToDTO : StrictTotalOrder _ _ _→ DecTotalOrder _ _ _
   stoToDTO sto =
                 record{ Carrier = Carrier
                       ; _≈_     = _≈_
                       ; _≤_     = _≤_
                       ; isDecTotalOrder = isDecTotalOrder }
   where
   open StrictTotalOrder sto using (_≈_; _<_; compare ...)
                    
   _≤_ : Rel Carrier _
   x ≤ y =  x < y ⊎ x ≈ y   -- **
   ...

I expect that  DecTotalOrder  can be proved for this _≤_ instance.
Right?

b) To use  Data.String.StrictTotalOrder,
   in which  _<_  is by the lexicographic comparison.
   I expect that this comparison is fast  (O(length string)).
   Is it? 

c) To apply  stoToDTO  to  Data.String.StrictTotalOrder  with 
   obtaining fast  DecTotalOrder  for String.

d) To implement  suc : String → String  as the lexicographically next
   string, and to use it for obtaining fast a list  xs : List String
with many different elements in  xs.

Is this plan correct? 
Can the goal be achieved in a simpler way?

First I thought of  Bin,  but then discovered that  _<_  is done there
by conversion to  Nat,  which is very expensive. 
Right?
So, I hope for  Data.String.StrictTotalOrder.

Who could advise, please?

Thanks,

------
Sergei