Theorem: Pos.one_pow (Extra/Pos/Lemmas.lean)

State before:
x : Nat
⊢ 1 ^ x = 1
Tactic:
exact Nat.one_pow ..
State after:
no goals