law pow_two_sym

bend-mathlib@0.8.1.0 · nat.bend:4883

import Base

4883# Squaring n gives n times n, reversed to rewrite toward the simple side.
4884law pow_two_sym:
4885  for n: Nat
4886  {Nat.mul(n, n) == Nat.pow(n, 2n) : Nat}