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

State before:
x y : Pos
⊢ x ≠ y + x
Tactic:
induction x with
| one =>
  apply Ne.symm
  exact Pos.succ_ne_one y
| succ x H =>
  intro h
  rw [Pos.add_succ] at h
  apply H
  exact Pos.add_right_cancel h
State after:
no goals

State before:
case one
y : Pos
⊢ 1 ≠ y + 1
Tactic:
apply Ne.symm
State after:
case one.h
y : Pos
⊢ y + 1 ≠ 1

State before:
case one.h
y : Pos
⊢ y + 1 ≠ 1
Tactic:
exact Pos.succ_ne_one y
State after:
no goals

State before:
case succ
y x : Pos
H : x ≠ y + x
⊢ x + 1 ≠ y + (x + 1)
Tactic:
intro h
State after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + (x + 1)
⊢ False

State before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + (x + 1)
⊢ False
Tactic:
rw [Pos.add_succ] at h
State after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ False

State before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ False
Tactic:
apply H
State after:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ x = y + x

State before:
case succ
y x : Pos
H : x ≠ y + x
h : x + 1 = y + x + 1
⊢ x = y + x
Tactic:
exact Pos.add_right_cancel h
State after:
no goals