calc
  _ ≃ abs (p^(step n'))  := eqv_refl
  _ ≃ abs (p^n' * p)     := abs_subst pow_step
  _ ≃ abs (p^n') * abs p := abs_compat_mul
  _ ≃ (abs p)^n' * abs p := mul_substL ih
  _ ≃ (abs p)^(step n')  := eqv_symm pow_step
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p : ℚ
n n' : ℕ
ih : abs (p ^ n') ≃ abs p ^ n'
⊢ abs (p ^ step n') ≃ abs p ^ step n'
no goals