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

State before:
a b c d : Int
⊢ (a > b) = (a - b > 0)
Tactic:
simp only [gt_iff_lt, eq_iff_iff]
State after:
a b c d : Int
⊢ b < a ↔ 0 < a - b

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

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

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

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