no goals
α : Type u
β : Type ?u.48263
inst✝ : OrderedRing α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ b = a + (b - a)
simp
α : Type u
β : Type ?u.48263
inst✝ : OrderedRing α
a✝ b✝ c✝ d a b : α
x✝ : ∃ c, c ≥ 0 ∧ b = a + c
c : α
hc : c ≥ 0
h : b = a + c
⊢ 0 ≤ c
α : Type u
β : Type ?u.48263
inst✝ : OrderedRing α
a✝ b✝ c✝ d a b : α
x✝ : ∃ c, c ≥ 0 ∧ b = a + c
c : α
hc : c ≥ 0
h : b = a + c
⊢ a ≤ b
rw [h, le_add_iff_nonneg_right]
no goals
α : Type u
β : Type ?u.48263
inst✝ : OrderedRing α
a✝ b✝ c✝ d a b : α
x✝ : ∃ c, c ≥ 0 ∧ b = a + c
c : α
hc : c ≥ 0
h : b = a + c
⊢ 0 ≤ c
exact hc