Theorem: Smt.Reconstruct.Arith.Real.neg_le_neg (Smt/Reconstruct/Arith/TightBounds/Lemmas.lean)

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ -a ≥ -b
Tactic:
simp
State after:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ a ≤ b

State before:
α : Type
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a ≤ b
⊢ a ≤ b
Tactic:
exact h
State after:
no goals