Re: [Agda] ... n ∸ m > 0

[Andrés Sicard-Ramírez]

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)


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150113/615bb36e/attachment.html