abs zpow

Stream: mathlib4

[Markus Schmaus]

What's the best way to prove this?

import Mathlib

example (x : Int) : |(2 : Rat) ^ x| = 2 ^ x := by
  sorry

I found docs#abs_pow, but no corresponding abs_zpow

[Damiano Testa]

Not sure if it is "best", but norm_num [zpow_nonneg] works.

[Vincent Beffara]

And so does simpa using zpow_nonneg zero_le_two _ which I guess is pretty much the same thing