Zulip Chat Archive

Stream: general

Topic: int.to_nat lemmas


view this post on Zulip Scott Morrison (Feb 13 2021 at 08:39):

I'm feeling sad about the lemmas about int.to_nat. Can someone suggest how to prove things like:

example (i : ) : i.to_nat - 1 = (i + -1).to_nat :=
sorry

view this post on Zulip Johan Commelin (Feb 13 2021 at 08:57):

I try to avoid to_nat whenever I can. int.nat_abs seems to have a better API

view this post on Zulip Johan Commelin (Feb 13 2021 at 08:57):

But I don't know if it makes sense to use that in your application

view this post on Zulip Yevhenii Diomidov (Feb 13 2021 at 19:55):

example (i : ) : i.to_nat - 1 = (i + -1).to_nat :=
by rcases i with (_ | _) | _; finish

Last updated: May 09 2021 at 19:11 UTC