[Agda] monot-minus for Nat

[Serge D. Mechveliani]

On Sat, Sep 15, 2012 at 07:29:09PM +0200, Nils Anders Danielsson wrote:
> On 2012-09-15 18:13, Serge D. Mechveliani wrote:
[..]
>> monot.-right : (k m n : Nat) -> k <= m -> k .- n <= m .- n
>
>> (1) Is there possible a simpler expression for  suc-comm, monot.-right ?
>
> [..]
> and a more general variant of monot.-right can be found in 
> Data.Nat.Properties  (???-mono).
>

I look into  Data.Nat.Properties  and see only these `-mono' :

  [n/2]-mono,  pred-mono,  _+-mono,  _*-mono_ 
 
pred-mono  may help, but does not look as a more general variant of 
           monot.-right.
(?)

Thanks,

------
Sergei