[Agda] direct product for list

[Serge D. Mechveliani]

Can you, please, answer a beginner question about the type for an 
ordered-list proof? 

First, I define of what is a  natural list ordered by <= : 
(for this letter I change  \bn -> Nat,  \<= to <=,  \_2 -> -2 ) 

  data OrderedList? : List Nat -> Set
       where
       nil    : OrderedList? []
       single : (x : Nat)  -> OrderedList? (x :: [])
       prep2  : (x y : Nat) -> (xs : List Nat) -> x <= y ->
                OrderedList? (y :: xs) -> OrderedList? (x :: y :: xs)

And I manage to use this definition in practice. For example,

  -- x :: xs  is ordered  ==>  xs  is ordered
  tailOrdered : {x : Nat} {xs : List Nat} -> OrderedList? (x :: xs) ->
                                                      OrderedList? xs
  tailOrdered (single _)                = nil
  tailOrdered (prep2 x y xs _ ord-y:xs) = ord-y:xs

  -- xs  is ordered  ==>  0 :: xs  is ordered
  prep0Ordered : {xs : List Nat} -> OrderedList? xs -> 
                                                  OrderedList? (0 :: xs)
  prep0Ordered nil                        = single 0
  prep0Ordered (single x)                 = prep2 0 x [] z<=n $ single x
  prep0Ordered (prep2 x y xs x<=y ord-y-xs) = 
                                            prep2 0 x (y :: xs) z<=n
                                            (prep2 x y xs x<=y ord-y-xs)


But then, I thought of the definition via the direct product (\times):

  OrderedList'? : List Nat -> Set
  OrderedList'? []             =  \top
  OrderedList'? (x :: [])      =  \top \times \top
  OrderedList'? (x :: y :: xs) =  x <= y \times (OrderedList'? (y :: xs))

It looks simpler, it does not introduce new constructors.
But I fail to process its data, so far. For example,

  tailOrdered' : {x : Nat} {xs : List Nat} -> OrderedList'? (x :: xs) ->
                                                        OrderedList'? xs
  tailOrdered' = proj-2

is not compiled: 
   OrderedList'? (.x :: .xs) !=< \Sigma _154 _155 of type Set
   when checking that the expression proj-2 has type
   OrderedList'? (.x :: .xs) -> OrderedList'? .xs

The expression   tailOrdered' ( _ , tl ) = tl                                

also is not compiled, it reports of a wrong pattern.

Is not  OrderedList'? (x :: xs)  a direct product of two types
(so that its member is a pair  ( _ , tl ) ) 
?
How to fix this?

Which definition of an  ordered natural list  is better to use?

Thank you in advance for explanation,

------
Sergei