Theorem: IMOSL.IMO2012A5.Case3.SCharNeTwo.map_add_one_eq_zero_imp (IMOSLLean4/IMO2012/A5/A5Cases/Case3.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : Ring R
inst✝² : CharTwo R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
hS : 2 ≠ 0
f : R → S
hf : ReducedGood f
x : R
h : f (x + 1) = 0
⊢ f (x * x) = -1
Tactic:
rw [Eq2_v2 hf.toNontrivialGood, h, sq, zero_mul, zero_sub]
State after:
no goals