θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k
θ ψ : ℝ
⊢ ↑(toIocMod two_pi_pos ψ θ) = ↑θ
rw [angle_eq_iff_two_pi_dvd_sub]
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k
refine' ⟨-toIocDiv two_pi_pos ψ θ, _⟩
no goals
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]