Zulip Chat Archive
Stream: Is there code for X?
Topic: x.pred < y.pred iff x < y
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?
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
Kenny Lau (Nov 26 2020 at 16:17):
PR
Eric Wieser (Nov 26 2020 at 16:21):
Is that a request or a status update?
Eric Wieser (Nov 26 2020 at 16:24):
Kenny Lau (Nov 26 2020 at 16:27):
A suggestion
Last updated: Dec 20 2023 at 11:08 UTC