law pow_two

bend-mathlib@0.8.1.0 · nat.bend:3764

import Base

3764# Squaring n gives n times n.
3765law pow_two:
3766  for n: Nat
3767  {Nat.pow(n, 2n) == Nat.mul(n, n) : Nat}