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