Theorem: IMOSL.IMO2012A5.QuasiPeriodic.iff_right2 (IMOSLLean4/IMO2012/A5/A5General/A5QuasiPeriodic.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : QuasiPeriodic f c
x : R
⊢ f (x + c) = f x * -f c ↔ f (x * c + 1) = 0
Tactic:
rw [mul_neg, hf.is_good, eq_neg_iff_add_eq_zero, add_comm]
State after:
no goals