# What am I doing wrong when proving the add_right_cancel theorem?

So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4.

I am currently trying to complete the Advanced Addition world so I can get access to the "≤ World"1 so I can more easily prove the clunky version of Fermat's Last Theorem2, and for some reason I am currently stuck on proving the add_right_theorem (Level 1 of Advanced Addition World), which states that$$a+n=b+n\implies a=b$$which I don't exactly know how I would state the proof or write it out in Lean4

Here's what I have done so far:

1. The first part (the proof by induction) is pretty easy. All I need to do is this:
induction n with d hd
repeat rw [add_zero]
intro h
exact h


however the second part$$a+\operatorname{succ}(d)=b+\operatorname{succ}(d)\implies a=b$$is where I am struggling. All I can do is add the successions together to rewrite it as$$\operatorname{succ}(a+d)=\operatorname{succ}(b+d)\implies a=b$$before being forced to introduce the hypothesis h to rewrite it as this:

hd: a + d = b + d → a = b
h: succ (a + d) = succ (b + d)
Goal: a = b


Now, when I apply succ_inj at h, it leaves me with

hd: a + d = b + d → a = b
h: a + d = b + d
Goal: a = b


and now I'm stuck, because I can't use decide since that returns the exact same thing, and triv doesn't work since the case "True" doesn't exist. (I got a bit desperate, sorry.)

Here is my proof so far:

induction n with d hd
repeat rw [add_zero]
intro h
exact h
repeat rw [add_succ]
intro h
apply succ_inj at h


So my question is: Where am I messing up the proof of the add_right_cancel theorem, and how should I actually go about proving it?

1I'll replace this with \le if it would look neater, the unicode for the "less than or equal to" symbol is u+00264 for anyone who wants to know.

2The more clunky version of Fermat's Last Theorem (that is, the first case of it) comes up in Power World level 10/10, and states that for no $$a,b,c,n\in\mathbb N$$,$$(a+1)^{n+3}+(b+1)^{n+3}=(c+1)^{n+3}$$which is where the Inequality World would come in handy, because it would greatly shorten the proof. The first case has been proven in Lean.

## 1 Answer

From

hd: a + d = b + d → a = b
h: a + d = b + d
Goal: a = b


you can use the apply tactic.