Theorem: Ideal.sub_mem_ofRel_of_rel (DividedPowers/DPAlgebra/Init.lean)

State before:
R✝ : Type u_1
M : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_3
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