[Agda] ... n ∸ m > 0

[Sergei Meshveliani]

On Mon, 2015-01-12 at 13:52 -0500, Andrés Sicard-Ramírez wrote:
> 
> On 12 January 2015 at 13:28, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Having the goal of  m < n → n ∸ m > 0   (for ℕ), 
>         
>         and using  Standard library 0.9,  I program
>         
>           lemma : ∀ n → (suc n) ∸ n ≡ 1
>           lemma 0       = PE.refl 
>           lemma (suc n) = lemma n
>         
>           m<n→n∸m>0 : ∀ {m n} → m < n → n ∸ m > 0
>           m<n→n∸m>0 {m} {n} m<n = 
>                             ≤begin  
>                               suc 0       ≡≤[ PE.sym $ lemma m ]
>                               suc m ∸ m    ≤[ ∸-mono m<n (≤refl {m}
>         PE.refl) ]  
>                               n ∸ m
>                             ≤end
>         
>         Here lemma looks like a complication that needs to be avoided.
>         Is there possible a shorter implementation for the goal?
> 

> ​Yes. You can pattern-match on m<n.​
> 


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


I suspect that using Standard library, an expression without recursion
is possible, even though being larger.
But this is a minor point, let it be.
 
------
Sergei