Zulip Chat Archive

Stream: general

Topic: is this true without decidable


view this post on Zulip Johan Commelin (Sep 07 2018 at 13:11):

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

view this post on Zulip Johan Commelin (Sep 07 2018 at 13:13):

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]?

view this post on Zulip Johan Commelin (Sep 07 2018 at 13:15):

Never mind. This is completely false.

view this post on Zulip Johan Commelin (Sep 07 2018 at 13:16):

/me needs to relearn modular arithmetic

view this post on Zulip Johan Commelin (Sep 07 2018 at 13:18):

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

view this post on Zulip Johan Commelin (Sep 07 2018 at 13:18):

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


Last updated: May 08 2021 at 18:17 UTC