Theorem: Smt.Arith.le_eq_sub_le_zero (Smt/Reconstruct/Arith/ArithPolyNorm.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ (a ≤ b) = (a - b ≤ 0)
Tactic:
simp only [tsub_le_iff_right, zero_add]
State after:
no goals