[Agda] (s ◃ m ) * (s' ◃ n)

[Sergei Meshveliani]

People,
I have a question about usage of Integer of Standard library.

Consider this trivial and naturally looking lemma: 

  lemma : (s s' : Sign) → (m n : ℕ) → 
          (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n), 

where  _*s_ = Sign._*_,  _*n_ = Nat._*_,  _*_ = Integer._*_. 

What can be a reasonably simple proof for it? 

This my proof is checked but looks rather complex:

----------------------------------------------------------------
lemma _ _  0 _ =  PE.refl
lemma s s' m 0 =  e           -- reduce to  "0 m"
  where
  e : (s ◃ m) * (+ 0) ≡ (s *s s') ◃ (m *n 0)
  e = ≡begin
        (s ◃ m) * (+ 0)        ≡[ *0 (s ◃ m) ]
        + 0                    ≡[ PE.sym $ 0* (s ◃ m) ]
        (+ 0) * (s ◃ m)        ≡[ PE.cong (\z → z * (s ◃ m)) $ ◃-0 s' ]
        (s' ◃ 0) * (s ◃ m)     ≡[ lemma s' s 0 m ]
        (s' *s s) ◃ (0 *n m)   ≡[ PE.cong (_◃_ (s' *s s)) $ 
                                                          *n-comm 0 m ]
        (s' *s s) ◃ (m *n 0)   ≡[ PE.cong (\sg → sg ◃ (m *n 0)) $
                                                         *s-comm s' s ]
        (s *s s') ◃ (m *n 0)
      ≡end

lemma s s' (sucN m) (sucN n) =
  ≡begin
    (s ◃ m') * (s' ◃ n')                                   ≡[ PE.refl ]

    (sign (s ◃ m') *s sign (s' ◃ n')) ◃ ((∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣))

                           ≡[ PE.cong (\sg → sg ◃ part2) $
                               PE.cong₂ _*s_ (sign-◃ s m) (sign-◃ s' n)
                            ]
    (s *s s') ◃ ((∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣))
                           ≡[ PE.cong (_◃_ (s *s s')) $
                               PE.cong₂ _*n_ (abs-◃ s m') (abs-◃ s' n')
                            ]
    (s *s s') ◃ (m' *n n')
  ≡end
  where
  m'    = sucN m
  n'    = sucN n
  part2 = (∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣)
------------------------------------------------------------------------

Also there are the two strange points. 

1) The part
 
      e 
   where
   e : ....
   e = 

needs to be skipped (as I usually do), so that the RHS to be just 
(begin ... end). 
But the checker   (MAlonzo of January 8, 2014)

does not allow this, showing      [ lemma s' s 0 m ]   with yellow
(probably a termination problem).
So that I have avoided a termination problem by a lucky occasion with 
extra  "e : ...".


2) In     ≡[ PE.cong (\z → z * (s ◃ m)) $ ◃-0 s' ]

  "◃-0 s'"  is a lemma which maps to  s' ◃ 0 ≡ + 0.
This is only by normalization, but the checker reports of unsolved metas
when I set  PE.refl  directly to the place. I tried adding hidden args
but failed.

Thank you in advance for your notes.

------
Sergei