[Agda] monot-minus for Nat

[Nils Anders Danielsson]

On 2012-09-15 18:13, Serge D. Mechveliani wrote:

> suc-comm : (m : Nat) -> (n : Nat) -> m + (suc n) == (suc m) + n

> monot.-right : (k m n : Nat) -> k <= m -> k .- n <= m .- n

> (1) Is there possible a simpler expression for  suc-comm, monot.-right ?

You can prove suc-comm using the ring solver (see README.Nat), and a
more general variant of monot.-right can be found in Data.Nat.Properties
(∸-mono).

> (2) The last pattern for  monot.-right  is not accessible, because
>      suc k <= m  = 0   is not satisfiable.
> How to skip this pattern? or at least -- how to reduce its RHS
> (for example by setting () in an appropriate place) ?

As follows:

   monot∸right (suc k) 0 (suc n) ()

-- 
/NAD