Theorem: Smt.Reconstruct.Int.le_eq_sub_le_zero (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
⊢ (a ≤ b) = (a - b ≤ 0)
Tactic:
apply propext
State after:
case a
a b c d : Int
⊢ a ≤ b ↔ a - b ≤ 0

State before:
case a
a b c d : Int
⊢ a ≤ b ↔ a - b ≤ 0
Tactic:
constructor
State after:
case a.mp
a b c d : Int
⊢ a ≤ b → a - b ≤ 0

case a.mpr
a b c d : Int
⊢ a - b ≤ 0 → a ≤ b

State before:
case a.mp
a b c d : Int
⊢ a ≤ b → a - b ≤ 0
Tactic:
exact Int.sub_nonpos_of_le
State after:
no goals

State before:
case a.mpr
a b c d : Int
⊢ a - b ≤ 0 → a ≤ b
Tactic:
exact Int.le_of_sub_nonpos
State after:
no goals