chore(analysis/complex/basic): golf `norm_rat/int/int_of_nonneg` (#12433)
chore(analysis/complex/basic): golf `norm_rat/int/int_of_nonneg` (#12433)

While looking at PR #12428, I found some easy golfing of some lemmas (featuring my first-ever use of `single_pass`! :smile: ).





leanprover-community/mathlib,leanprover-community/mathlib