Theorem: Smt.Reconstruct.Int.lt_eq_sub_lt_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:
apply Int.sub_neg_of_lt
State after:
no goals

State before:
case a.mpr
a b c d : Int
⊢ a - b < 0 → a < b
Tactic:
apply Int.lt_of_sub_neg
State after:
no goals