[Agda] monot-minus for Nat

[Serge D. Mechveliani]

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