case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖Quot.mk Setoid.r x‖ ≤ abs p / 2
p : ℝ
x : AddCircle p
hp : p ≠ 0
⊢ ‖x‖ ≤ abs p / 2
obtain ⟨x⟩ := x
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ abs p / 2
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖Quot.mk Setoid.r x‖ ≤ abs p / 2
change ‖(x : AddCircle p)‖ ≤ |p| / 2
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ abs (p⁻¹ * x - ↑(round (p⁻¹ * x))) ≤ 1 / 2
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ abs p / 2
rw [norm_eq, ← mul_le_mul_left (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub, mul_left_comm,
  ← mul_div_assoc, ← abs_mul, inv_mul_cancel hp, mul_one, abs_one]
no goals
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ abs (p⁻¹ * x - ↑(round (p⁻¹ * x))) ≤ 1 / 2
exact abs_sub_round (p⁻¹ * x)