Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_of_ne_zero (IMOSLLean4/Extra/F2X/Defs.lean)

State before:
n : ℕ
P : 𝔽₂X
h : n ≠ 0
⊢ P.natPow n = if n % 2 = 0 then P.square.natPow (n / 2) else P.square.natPow (n / 2) * P
Tactic:
rw [𝔽₂X.natPow, if_neg h]
State after:
no goals