Zulip Chat Archive

Stream: Is there code for X?

Topic: x.pred < y.pred iff x < y


view this post on Zulip Eric Wieser (Nov 26 2020 at 16:11):

My goal has once again got stuck in a "should be obvious" state:

n : ,
x y : fin n.succ,
h : x < y,
hx : ¬x = 0
 x.pred hx < y.pred _

What can I do to progress?

view this post on Zulip Eric Wieser (Nov 26 2020 at 16:16):

rw [←fin.succ_lt_succ_iff, fin.succ_pred, fin.succ_pred]

Guess we need a fin.pred_lt_pred_iff to match docs#fin.succ_lt_succ_iff

view this post on Zulip Kenny Lau (Nov 26 2020 at 16:17):

PR

view this post on Zulip Eric Wieser (Nov 26 2020 at 16:21):

Is that a request or a status update?

view this post on Zulip Eric Wieser (Nov 26 2020 at 16:24):

#5121

view this post on Zulip Kenny Lau (Nov 26 2020 at 16:27):

A suggestion


Last updated: May 07 2021 at 22:14 UTC