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

State before:
k m : ℕ
⊢ Xpow (k + m) = Xpow k * Xpow m
Tactic:
rw [← XpowMul_eq_Xpow_mul, XpowMul_Xpow, add_comm]
State after:
no goals