θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ abs (cos θ) = abs (cos ψ)
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ abs (cos θ) = abs (cos ψ)
simp_rw [two_zsmul, ← two_nsmul] at h
no goals
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ abs (cos θ) = abs (cos ψ)
exact abs_cos_eq_of_two_nsmul_eq h