Theorem: IMOSL.IMO2012A5.𝔽₃.cast_add (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/F3.lean)

State before:
R : Type u_1
inst✝ : AddGroupWithOne R
h : 3 = 0
x y : 𝔽₃
⊢ 1 + 1 = -1
Tactic:
rwa [one_add_one_eq_two, eq_neg_iff_add_eq_zero, two_add_one_eq_three]
State after:
no goals