[Agda] ... n ∸ m > 0

[Sergei Meshveliani]

On Tue, 2015-01-13 at 13:30 -0500, Andrés Sicard-Ramírez wrote:
> 
> On 13 January 2015 at 12:47, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Thank you.
>         Indeed:
>         
>          m<n→n∸m>0 {0}     {suc n} _             =  suc>0
>          m<n→n∸m>0 {0}     {0}     ()
>          m<n→n∸m>0 {suc m} {suc n} (s≤s suc-m≤n) =  m<n→n∸m>0 {m} {n}
>         suc-m≤n
> 
> ​A version using only two equations:
> 
> ​m<n→n∸m>0 : ∀ {m n} → m < n → n ∸ m > 0
> m<n→n∸m>0 (s≤s z≤n)     = s≤s z≤n
> m<n→n∸m>0 (s≤s (s≤s h)) = m<n→n∸m>0 (s≤s h)
> 

Great! Thank you.

------
Sergei