[Agda] monot-minus for Nat

[Serge D. Mechveliani]

People,
I have a couple of beginner questions about usage of Standard Library
(in Agda-2.3.0.1, lib-0.6).
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

-- with using Standard Library as possible. 
For this letter I apply the following denotations:

 \bn -> Nat,    \equiv -> ==,   \<=  ->  <=,    \.-  ->  .-
 (for writing math symbols under the mutt e-mail program)
 ,
 Relation.Binary.PropositionalEquality as PropEq,
 <=trans = let open DecTotalOrder hiding ( _<=_ )
           in  IsDecTotalOrder.trans $ isDecTotalOrder Nat.decTotalOrder
 +comm = IsCommutativeMonoid.comm  +isComMon 
         where
         natIsCommSemir = NatProp.isCommutativeSemiring
         +isComMon      = IsCommutativeSemiring.+-isCommutativeMonoid 
                                                  natIsCommSemir
I program:
------------------------------------------------------------------------
suc-comm : (m : Nat) -> (n : Nat) -> m + (suc n) == (suc m) + n
suc-comm m n =  PropEq.trans (PropEq.trans p1 p2) refl
              where
              p1 = +comm m (suc n)       -- : m + (suc n) == suc (n + m)     
              p2 = cong suc $ +comm n m  -- : suc (n + m) == suc (m + n) 

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

-- below  "_'"  denotes  suc_                                                 
monot.-right 0       m       n       _      = <=trans (n.-m<=n n 0) z<=n
monot.-right _       _       0       k<=m   = k<=m 
monot.-right (suc k) (suc m) (suc n) k'<=m' = monot.-right k m n k<=m
                                              -- k'<=m' : suc k <= suc m      
                                        where
                                        k<=m = cancel-+-left-<= 1 k'<=m'

monot.-right (suc k) 0       (suc n) k'<=0  =
                                         -- unaccessibe, due to  k' <= 0

                                <=trans  k'.-n'<=0  z<=n
                                where
                                k'.-n'<=k' =  n.-m<=n (suc n) (suc k)
                                k'.-n'<=0  =  <=trans  k'.-n'<=k'  k'<=0
------------------------------------------------------------------------

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

(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) ?

Thank you in advance for explanation,

------
Sergei