Given (a : Z) and (a >= 0), I would like to have (n : N) such that n = a. This is of course a bit troublesome because n = a is heterogeneous equality.
I have found nat_abs which does something like this except it also handles the case when I have a negative whole number, which I know that I don't.
How does one deal with this situation in Lean?
n = a isn't a heterogeneous equality, since you (hopefully) can't prove N = Z. The best you can hope for is int.of_nat n = a, and you should be able to prove from a >= 0 that int.of_nat (nat_abs a) = a.
Note that you can write a = n, and it will type check, because Lean will coerce n to int.of_nat n. This is not a heterogeneous equality, it's a normal equality in Z.