Help with advanced addition level 13

Stream: new members

[Mujtaba Alam]

The goal is ⊢ n ≠ succ n. Here's what I have so far:

cases n with d,
intro h,
exact zero_ne_succ 0 h,


intro h,
rw ← add_one_eq_succ at h,
rw ← add_one_eq_succ at h,
rw add_right_cancel_iff at h,

Now I have h : d = d + 1 and my goal is false. Can someone give me a hint? Maybe add_zero and zero_ne_one? I'm hitting a wall here

[Riccardo Brasca]

This goal looks like the original one, doesn't it?

[Ruben Van de Velde]

Given an assumption that n+0 = n+1, can you prove that 0=1?