Theorem: Pos.lt_add_right (Extra/Pos/Lemmas.lean)

State before:
x y : Pos
⊢ x < x + y
Tactic:
induction y with
| one => exact Pos.lt_succ_self x
| succ y H => apply Pos.lt_trans H; rw [Pos.add_succ]; exact Pos.lt_succ_self (x + y)
State after:
no goals

State before:
case one
x : Pos
⊢ x < x + 1
Tactic:
exact Pos.lt_succ_self x
State after:
no goals

State before:
case succ
x y : Pos
H : x < x + y
⊢ x < x + (y + 1)
Tactic:
apply Pos.lt_trans H
State after:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + (y + 1)

State before:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + (y + 1)
Tactic:
rw [Pos.add_succ]
State after:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + y + 1

State before:
case succ
x y : Pos
H : x < x + y
⊢ x + y < x + y + 1
Tactic:
exact Pos.lt_succ_self (x + y)
State after:
no goals