Zulip Chat Archive

Stream: general

Topic: succ_pred_eq_of_pos

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 13:46):

succ_pred_eq_of_pos says n > 0 → succ (pred n) = n and it's in core Lean. I just applied it and ended up with a goal card s > 0 with s a multiset, and then I tried to rewrite multiset.card_pos_iff_exists_mem but the rewrite fails because the hypothesis is 0 < card s. That's kind of annoying and it's not the first time today that this has happened to me. I feel like succ_pred_eq_of_pos should say 0 < n → succ (pred n) = n but I guess there's nothing that can be done about this? Or am I missing a trick? Currently I'm just using show to rewrite the goal so it uses <.

Last updated: May 13 2021 at 18:26 UTC