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

State before:
case zero_right
z : Nat
hz : z > 0
x : Nat
⊢ x - 0 < z ↔ x < 0 + z
Tactic:
rw [Nat.sub_zero, Nat.zero_add]
State after:
no goals

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

State before:
case zero_left
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z ↔ 0 < y + z
Tactic:
constructor
State after:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z → 0 < y + z

case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
⊢ 0 < y + z → 0 < z

State before:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
⊢ 0 < z → 0 < y + z
Tactic:
intro
State after:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < y + z

State before:
case zero_left.mp
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < y + z
Tactic:
transitivity z using LT.lt, LE.le
State after:
case zero_left.mp.left
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < z

case zero_left.mp.right
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ z ≤ y + z

State before:
case zero_left.mp.left
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ 0 < z
Tactic:
exact hz
State after:
no goals

State before:
case zero_left.mp.right
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < z
⊢ z ≤ y + z
Tactic:
exact Nat.le_add_left ..
State after:
no goals

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

State before:
case zero_left.mpr
z : Nat
hz : z > 0
y : Nat
a✝ : 0 < y + z
⊢ 0 < z
Tactic:
exact hz
State after:
no goals

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

State before:
case succ_succ
z : Nat
hz : z > 0
x y : Nat
H : x - y < z ↔ x < y + z
⊢ x - y < z ↔ x < y + z
Tactic:
apply H
State after:
no goals