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

[Andrés Sicard-Ramírez]

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.​



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