How do I convert a positive integer to a natural number?

Stream: new members

[Lars Ericson]

Lean is not letting me express this:

lemma simp_rat_abs (a: ℤ) (h: a ≥ 0) : a.nat_abs = coe ℤ ℕ a

I can't find a match in mathlib.

[Johan Commelin]

lift a to nat using h

[Lars Ericson]

I'm in a goal state

⊢ 4 = 21.nat_abs.gcd 4

I guess I need to give a name to 21 and then prove it is greater than 0 before applying the lift? Note: ring and simp don't do anything to this. I hoping for false.

[Lars Ericson]

In other words I want to rewrite this to

⊢ 4 = 21.gcd 4

and then start grinding away on the value of 21.gcd 4 but I think I need to convert the 21 to nat before grinding.