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

State before:
a b c d : Int
⊢ (a = b) = (a - b = 0)
Tactic:
simp only [Int.sub_eq_zero]
State after:
no goals