x : ℂ
hi : 0 < x.im
⊢ -arccos ((-x).re / ↑abs (-x)) = arccos (x.re / ↑abs x) - π
x : ℂ
hi : 0 < x.im
⊢ arg (-x) = arg x - π
rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]
no goals
x : ℂ
hi : 0 < x.im
⊢ -arccos ((-x).re / ↑abs (-x)) = arccos (x.re / ↑abs x) - π
simp [neg_div, Real.arccos_neg]