[Agda] ... n ∸ m > 0

[Sergei Meshveliani]

People,

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?

Thanks,

------
Sergei
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150112/8425129e/attachment.html