[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : StrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0
[PROOFSTEP]
simpa
  -- used alongside `mul_neg` and `mul_nonpos`, so has the same argument pattern for uniformity
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
x✝ : R a 0
h : b = 0
⊢ a * b = 0
[PROOFSTEP]
simp [h]
  -- used in the `nlinarith` normalization steps. The `_` argument is for uniformity.
[GOAL]
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
h : a = 0
x✝ : R b 0
⊢ a * b = 0
[PROOFSTEP]
simp [h]
