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

State before:
n : ℕ
P : 𝔽₂X
h : P.square = P * P
⊢ (Xpow n + P).square = (Xpow n + P) * (Xpow n + P)
Tactic:
rw [square_add, square_Xpow, 𝔽₂X.add_mul, 𝔽₂X.mul_add, ← Xpow_add, Nat.two_mul,
  𝔽₂X.mul_add, ← h, ← P.mul_comm, CharTwo.add_add_add_cancel_middle]
State after:
no goals