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

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

State before:
case one
x : Pos
⊢ x < 1 + x
Tactic:
rw [Pos.one_add_eq_add_one]
State after:
case one
x : Pos
⊢ x < x + 1

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 < y + x
⊢ x < y + 1 + x
Tactic:
apply Pos.lt_trans H
State after:
case succ
x y : Pos
H : x < y + x
⊢ y + x < y + 1 + x

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

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