[Agda] _<=_ and _<_

[Sergei Meshveliani]

On Tue, 2013-09-24 at 17:18 +0400, Sergei Meshveliani wrote:
> People, I have a couple of questions about general relation between 
>                                                             _≤_ and _<_ 
> in the  lib-0.7 standard library.
> 
> 1. What is the most general situation in  lib-0.7  under which these
> usual properties can be proved:
>                                        
>                        x ≤ y  iff  x < y ⊎ x ≈ y               (I),
>                        x < y  ->  ¬ y ≤ x                      (II)
> ?
> 
> 2. For  Nat,  
>    it is natural to derive (I) and (II) from  DecTotalOrder,
>    as a specialization of the above generic laws. 
> 
> But  DecTotalOrder  says nothing about  _<_.
> Then, we are forced to derive (I) and (II) from the union of
> DecTotalOrder and StrictTotalOrder.
> Right?
> 
> Well,  Data.Nat  has  decTotalOrder.  But it is silent about 
> Strict(Total)Order.


Sorry, I see now   Data.Nat.Properties.strictTotalOrder

This withdraws the question 2.
The questions 1 and 3 remain.

Regards,

------
Sergei