[Agda] double constructor termination

[Sergei Meshveliani]

Hi,  

Can people advise, please, on the following subject?
The below program can be rewritten with removing a double `suc' pattern.
But let it be a contrived example:

------------------------------------------------------------------
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Nat using (ℕ; suc; _+_; _≤_; pred)

open _≤_

lemma :  ∀ n → n ≤ n + 1
lemma 0             =  z≤n
lemma 1             =  s≤s z≤n
lemma (suc (suc n)) =  s≤s n'≤n'+1  where
                                    n'≤n'+1 = lemma (suc n)
------------------------------------------------------------------

Agda does not see termination here.
What is the nicest way to prove termination with preserving this suc-suc
pattern?
I write it this way: 

--------------------------------
lemma n =  aux n (pred n) PE.refl
  where
  aux : (n m : ℕ) → m ≡ pred n → n ≤ n + 1
  aux 0             _  _    =  z≤n
  aux 1             _  _    =  s≤s z≤n
  aux (suc (suc n)) 0  ()
  aux (suc (suc n)) (suc m) m'≡pred-n'' =  s≤s n'≤n'+1
                               where
                               m≡pred-n' = PE.cong pred m'≡pred-n''
                               n'≤n'+1   = aux (suc n) m m≡pred-n'
---------------------------------

And it looks awkward.

Thanks, 

------
Sergei