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

State before:
a b c d : Int
⊢ (a ≥ b) = (a - b ≥ 0)
Tactic:
simp only [ge_iff_le, 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_nonneg_of_le
State after:
no goals

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