Nat from int and nonneg proof

Stream: new members

[Bjørn Kjos-Hanssen]

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]

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]

Thanks, by omega did it!