no goals
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p
rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]