コラッツ予想がとけたらいいな2

自分の考察を書いていきます。

(-1)*(-1) = 1

足し算の定義:0と−が存在して結合法則と交換法則を満たすような演算のことを足し算と呼ぶ

(-1)×(-1)=1の数学的証明が凄すぎて大草原 | 不思議.net

ここを見て、Agdaで(-1)*(-1) = 1を証明したいと思った。
いちおうできた。
Agda/integer7.agda at master · righ1113/Agda · GitHub
(nat, nat)で整数を表現すると、整数の積の定義が
(x, y)*(z, w) = (x * z + y * w, x * w + y * z)になる。
するとrefl一発で解けてしまった(minus1)。そりゃそうだ。
よく分からないので、PropEq.≡-Reasoningでもやってみた(minus2)。
出来たから良いけど、minus1の正当性が分からないなあ。