## Stream: new members

### Topic: How do I convert a positive integer to a natural number?

#### Lars Ericson (Jan 18 2021 at 17:53):

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 (Jan 18 2021 at 17:53):

lift a to nat using h

#### Lars Ericson (Jan 18 2021 at 17:57):

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 (Jan 18 2021 at 18:04):

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.

Last updated: May 06 2021 at 22:13 UTC