[Agda] Sign.+ ◃

[Sergei Meshveliani]

People,
For a certain evident lemma for  Integer._*_  and  _*n_ = Nat._*_, 
I write

-------------------------------------------
+◃ : (n : ℕ) → (Sign.+ ◃ n) ≡ + n
+◃ 0        = refl
+◃ (sucN _) = refl

+n*+q=+m :  (m n q : ℕ) →  n *n q ≡ m  →  (+ n) * (+ q) ≡ (+ m)
+n*+q=+m m n q n*q=m =
           ≡begin  (+ n) * (+ q)       ≡[ refl ]
                   Sign.+ ◃ (n *n q)   ≡[ cong (_◃_ Sign.+) n*q=m ]
                   Sign.+ ◃ m          ≡[ +◃ m ]
                   + m
           ≡end
-------------------------------------------

The necessity of setting  ≡[ +◃ m ]   instead of just skipping this line
looks strange, as well as the lemma of  +◃.

I suspect that this is due to a particular pattern order in the
implementation for  Integer._◃_.  
May be it is better to move the pattern with   ... zero  
to the second place? 

Or may be, my code can be simplified?

Thanks,

------
Sergei