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

State before:
x y : Nat
⊢ x > 0 → y > 0 → x - y < x
Tactic:
intro hx hy
State after:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x - y < x

State before:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x - y < x
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos]
State after:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x < y + x

case hz
x y : Nat
hx : x > 0
hy : y > 0
⊢ x > 0

State before:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x < y + x
Tactic:
exact Nat.lt_add_of_pos_left hy
State after:
no goals

State before:
case hz
x y : Nat
hx : x > 0
hy : y > 0
⊢ x > 0
Tactic:
exact hx
State after:
no goals