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

State before:
x y z : Nat
hpos : y > 0
⊢ x < y + z → x - z < y
Tactic:
intro h
State after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x - z < y

State before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x - z < y
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos]
State after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < z + y

case hz
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ y > 0

State before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < z + y
Tactic:
rw [Nat.add_comm]
State after:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < y + z

State before:
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ x < y + z
Tactic:
exact h
State after:
no goals

State before:
case hz
x y z : Nat
hpos : y > 0
h : x < y + z
⊢ y > 0
Tactic:
exact hpos
State after:
no goals