[Agda] `using (DecTotalOrder)'

[Serge D. Mechveliani]

Can you, please, tell how to import  DecTotalOrder  with `using' ?

(Agda-2.3.0.1, MAlonzo, 
 record DecTotalOrder ...   defined in  Relation.Binary  of Standard
 Library  lib-0.6
)

---------------------------------
module OrdList where
open import Relation.Nullary using ( Dec; yes; no )
open import Relation.Binary  using ( DecTotalOrder )
...

open DecTotalOrder
data OrderedList? {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2) :
                  List $ Carrier ord -> Set $ L-suc $ max c $ max l1 l2
  where
  ...
  cons : let A = Carrier ord
         in
         (x y : A) -> (xs : List A) -> _<=_ ord x y ->
         OrderedList? ord (y :: xs) -> OrderedList? ord (x :: y :: xs)
----------------------------------

(for this letter I replace the math symbols  \<= to <=,  \:: to :: ). 

The checker reports 
"No such module  DecTotalOrder  when scope checking the declaration
   open DecTotalOrder
"
If I remove  ``using ( DecTotalOrder )'',  then it does type-check.
But for most modules M, I would like to restrict explicitly, what is 
used from M. 

Question 2:
how to omit here the argument  ord  in  ``_<=_ ord x y''  ?
For it is said that  dep.records + hidden agruments  stands for type 
classes.
Currently I do not think that it is crucial, but for curiosity.

Thank you in advance for explanation,

-------
Sergei