Theorem: Nat.lt_sub_iff_add_lt (GMLInit/Data/Nat/Sub.lean)

State before:
x y z : Nat
⊢ x < y - z ↔ x + z < y
Tactic:
induction y, z with
| zero_right y => rw [Nat.sub_zero, Nat.add_zero]
| zero_left z => rw [Nat.zero_sub]; constructor <;> (intro; contradiction)
| succ_succ y z H => rw [Nat.succ_sub_succ, Nat.add_succ, Nat.succ_eq, Nat.succ_lt_succ_iff]; exact H
State after:
no goals

State before:
case zero_right
x y : Nat
⊢ x < y - 0 ↔ x + 0 < y
Tactic:
rw [Nat.sub_zero, Nat.add_zero]
State after:
no goals

State before:
case zero_left
x z : Nat
⊢ x < 0 - z ↔ x + z < 0
Tactic:
rw [Nat.zero_sub]
State after:
case zero_left
x z : Nat
⊢ x < 0 ↔ x + z < 0

State before:
case zero_left
x z : Nat
⊢ x < 0 ↔ x + z < 0
Tactic:
constructor <;> (intro; contradiction)
State after:
no goals

State before:
case zero_left.mpr
x z : Nat
⊢ x + z < 0 → x < 0
Tactic:
intro
State after:
case zero_left.mpr
x z : Nat
a✝ : x + z < 0
⊢ x < 0

State before:
case zero_left.mpr
x z : Nat
a✝ : x + z < 0
⊢ x < 0
Tactic:
contradiction
State after:
no goals

State before:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y + 1 - (z + 1) ↔ x + (z + 1) < y + 1
Tactic:
rw [Nat.succ_sub_succ, Nat.add_succ, Nat.succ_eq, Nat.succ_lt_succ_iff]
State after:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y - z ↔ x + z < y

State before:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y - z ↔ x + z < y
Tactic:
exact H
State after:
no goals