Zulip Chat Archive

Stream: new members

Topic: Nat from int and nonneg proof

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?

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.

Bjørn Kjos-Hanssen (Dec 27 2020 at 00:03):

Thanks, by omega did it!

Last updated: Dec 20 2023 at 11:08 UTC