# [Agda] monot-minus for Nat

Serge D. Mechveliani mechvel at botik.ru
Sat Sep 15 19:07:05 CEST 2012

```On Sat, Sep 15, 2012 at 08:13:36PM +0400, Serge D. Mechveliani wrote:
> [..]
> I need Agda proofs for
>                    (m : Nat) -> (n : Nat) -> m + (suc n) == (suc m) + n,
>                    (k m n : Nat) -> k <= m ->  k .- n <= m .- n
> [..]
> monot.-right 0       m       n       _      = <=trans (n.-m<=n n 0) z<=n
> [..]
>
> (1) Is there possible a simpler expression for  suc-comm, monot.-right ?
> [..]

Before writing recursion for  monot.-right  I planned the following human
proof.
If  n >= k  then  k .- n == 0  <=  m .- n
else
n < k, n < m;
(i)   k .- n <= m .- n   implies   n + (k .- n) <= n + (m .- n)
by +-monotonicity-<=;

(ii)  n + (k .- n) <= n + (m .- n)   implies  k .- n <= m .- n,
because otherwise   k .- n > m .- n,   n + (k .- n) > n + (m .- n)
by +-monotonicity->,  and this contradicts to  (i);

(iii) n + (k .- n) == k,    n + (m .- n) == m;

(iv)  By (iii),  (ii) is reduced to  k <= m  ==>  k .- n <= m .- n

But I do not see, so far, how to implement the part of
``otherwise ... contradicts to  (i)''.

Thanks,

------
Sergei
```