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

State before:
x y z : Nat
hx : x > y
hz : y < z
⊢ z - x < z - y
Tactic:
apply Nat.sub_lt_of_pos_of_lt_add
State after:
case hpos
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y > 0

case a
x y z : Nat
hx : x > y
hz : y < z
⊢ z < z - y + x

State before:
case hpos
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y > 0
Tactic:
apply Nat.sub_pos_of_lt
State after:
case hpos.h
x y z : Nat
hx : x > y
hz : y < z
⊢ y < z

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

State before:
case a
x y z : Nat
hx : x > y
hz : y < z
⊢ z < z - y + x
Tactic:
transitivity (y + (z - y)) using LE.le, LT.lt
State after:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ y + (z - y)

case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ y + (z - y) < z - y + x

State before:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ y + (z - y)
Tactic:
rw [Nat.add_sub_comm]
State after:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ z + (y - z)

State before:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ z + (y - z)
Tactic:
exact Nat.le_add_right ..
State after:
no goals

State before:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ y + (z - y) < z - y + x
Tactic:
rw [Nat.add_comm]
State after:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y + y < z - y + x

State before:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y + y < z - y + x
Tactic:
exact Nat.add_lt_add_left hx ..
State after:
no goals