私は次のことを証明しようとしています：
1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1
1-pow {zero} = refl
1-pow {suc x} = {!!}
私は Adga を初めて使用し、どこから始めればよいかさえわかりません。提案やガイダンスはありますか？明らかに、紙の上で証明するのは非常に簡単ですが、Agda に何を伝えればよいかわかりません。
pow 関数を次のように定義しました。
_pow_ : ℕ → ℕ → ℕ
x pow zero = 1
x pow (suc zero) = x
x pow (suc y) = x * (x pow y)