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

State before:
case zero
x y : Nat
⊢ x - y < 0 → x < y + 0
Tactic:
intro
State after:
case zero
x y : Nat
a✝ : x - y < 0
⊢ x < y + 0

State before:
case zero
x y : Nat
a✝ : x - y < 0
⊢ x < y + 0
Tactic:
contradiction
State after:
no goals

State before:
case succ
x y z : Nat
⊢ x - y < z + 1 → x < y + (z + 1)
Tactic:
intro h
State after:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x < y + (z + 1)

State before:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x < y + (z + 1)
Tactic:
rw [←Nat.sub_lt_iff_lt_add_of_pos]
State after:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x - y < z + 1

case succ.hz
x y z : Nat
h : x - y < z + 1
⊢ z + 1 > 0

State before:
case succ
x y z : Nat
h : x - y < z + 1
⊢ x - y < z + 1
Tactic:
exact h
State after:
no goals

State before:
case succ.hz
x y z : Nat
h : x - y < z + 1
⊢ z + 1 > 0
Tactic:
exact Nat.zero_lt_succ ..
State after:
no goals