[Agda] Bin._<_

[Serge D. Mechveliani]

People,
I have a beginner question. Probably, it is on usage of  lib-0.6.

Please, what stands for "<" for Bin  (binary naturals) ?
I need to test a binary variant for `length' and `lookup':

-----------------------------------------------------------------
module Lookup where
open import Data.Bool
open import Data.Bool.Show
open import Data.Char
open import Data.String
open import Data.List
open import Data.Nat
open import Data.Bin as Bin
open import Foreign.Haskell
open import IO.Primitive
open import Prelude using (showBin)   --

aParticularList1 : List Char
aParticularList1 = 'a' Б┬╥ 'b' Б┬╥ 'c' Б┬╥ 'd' Б┬╥ []   -- this is `::'

bLength : {A : Set} -> List A -> Bin
bLength []       = 0#
bLength (x Б┬╥ xs) = Bin.suc (bLength xs) 

l : Bin   
l = bLength aParticularList1

b : Bool
b = 0# Bin._<_ l   -- trying to compare binary naturals

lookup : {A : Set}(xs : List A)(n : Bin) -> (T (n < (bLength xs))) -> A
lookup []       n    ()         
lookup (x Б┬╥ xs) zero p  = x     
lookup (x Б┬╥ xs) n    p  = lookup xs (pred n) p  

main : IO Unit
main =  putStrLn (toCostring (show b))
-------------------------------------------------------

`0# Bin._<_ l'  looks like an error, because  Bin._<_  is, probably,
                a type (?)

Can the library have the same symbol _>_ to use for comparison on
Nat, Bin, Integer ?

Another question:  where is explained the meaning of the word `using' 
                   in the import declaration?

Thank you in advance for explanation,

-------
Sergei