Theorem: IMOSL.Extra.CharTwo.add_one_sq (IMOSLLean4/Extra/CharTwo/Ring/Basic.lean)

State before:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharTwo R
x : R
⊢ (x + 1) ^ 2 = x ^ 2 + 1
Tactic:
rw [sq, sq, add_one_mul_self]
State after:
no goals