is this true without decidable

Stream: general

[Johan Commelin]

example (R : Type) [ring R] (i j : ℕ) (hnat : i ≠ j)
(hR : ((i : R) + 1) = ((j : R) + 1)) :
((1 : R) = (0 : R)) := sorry

[Johan Commelin]

If it is true, what is the one-line proof?
If it is not true, what is the one-line proof assuming [decidable_eq R]?

[Johan Commelin]

Never mind. This is completely false.

[Johan Commelin]

/me needs to relearn modular arithmetic

[Johan Commelin]

I thought this was my goal state. But it's not. i and j are coerced somewhere else. But I don't know where.

[Johan Commelin]

/me needs to look at the pp.all true variant of the goal state.