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

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

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

State before:
case one.h
y : Pos
⊢ 1 + y ≠ 1
Tactic:
rw [Pos.one_add_eq_add_one]
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 ≠ x + y
⊢ x + 1 ≠ x + 1 + y
Tactic:
intro h
State after:
case succ
y x : Pos
H : x ≠ x + y
h : x + 1 = x + 1 + y
⊢ False

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

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

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