Theorem: Ideal.sub_mem_ofRel_of_rel (unused_files/Init_copy.lean)

State before:
R✝ : Type ?u.35137
M : Type ?u.35140
inst✝³ : CommRing R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : Ring R
r : R → R → Prop
a b : R
hr : r a b
⊢ a - b + b = a
Tactic:
rw [sub_add_cancel]
State after:
no goals