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

State before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * n + 1) = P.square.natPow n * P
Tactic:
rw [P.natPow_of_ne_zero (2 * n).add_one_ne_zero, Nat.mul_add_mod,
  Nat.mul_add_div Nat.two_pos, if_neg Nat.one_ne_zero,
  Nat.div_eq_of_lt Nat.one_lt_two, Nat.add_zero]
State after:
no goals