p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = abs p * abs (p⁻¹ * x - ↑(round (p⁻¹ * x)))
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = p * abs (p⁻¹ * x - ↑(round (p⁻¹ * x)))
conv_rhs =>
  congr
  rw [← abs_eq_self.mpr hp.le]
no goals
p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = abs p * abs (p⁻¹ * x - ↑(round (p⁻¹ * x)))
rw [← abs_mul, mul_sub, mul_inv_cancel_left₀ hp.ne.symm, norm_eq, mul_comm p]