[Agda] assoc Sign._*_

[Sergei Meshveliani]

People,

this is a question on Data.Sign of Standard library.

I use the lemmata like  {s s'} : Sign -> s *s (s' *s s) ≡ s'
for _*s_ = Sign._*_.

For these lemmata, I prove  associativity for  _*s_ 
(spending 8 patterns) and commutativity.

But is not it natural for these two laws to be in
Data.Sign.Properties ?

Regards,

------
Sergei