Zulip Chat Archive

Stream: new members

Topic: Nat from int and nonneg proof


view this post on Zulip Bjørn Kjos-Hanssen (Dec 26 2020 at 23:47):

Is there a way to take an int and a proof that it's nonnegative and cast it into a nat?
More specifically, if I have natural numbers n k and a proof of k+1 \le n, how to prove that n- (k+1)+1 = n-k?

view this post on Zulip Rob Lewis (Dec 26 2020 at 23:55):

These seem like two different questions, but: see tactic#lift for the first, tactic#omega and tactic#zify for the second.

view this post on Zulip Bjørn Kjos-Hanssen (Dec 27 2020 at 00:03):

Thanks, by omega did it!


Last updated: May 13 2021 at 06:15 UTC