Please take the definitions from the attached ArcCosCos file. Errors occur when copying into a text window.

IMHO A function in Wolfram is nothing more than its definition. Therefore, proving the equality of two functions is nothing more than establishing the equivalence of their definitions.

As they say in my language: It was a long time ago and not true. I have long since corrected it. Check the attached file ArcCosCos, please. Copying to text causes errors.

And I remember your trick with ArcTan[1/x] + ArcTan[x]. Bravo! I've never seen that before anywhere. If there is any literature on this subject, please tell me.

First, let me corrected the syntax error of enclosing Pi in square brackets:

f[x_] := Which[
  0 <= Mod[x, 2 Pi] < Pi, Mod[x, Pi], 
  Pi <= Mod[x, 2 Pi] < 2 Pi, Mod[-x, Pi]
]
g[x_] := Pi (1 - (-1)^Quotient[x, Pi])/2 + (-1)^Quotient[x, Pi] Mod[x, Pi]

Then, checking equality of f[x] and g[x] over a range of values for x:

Table[f[x], {x, -10, 10, 1/10}] == Table[g[x], {x, -10, 10, 1/10}]
(* True *)

Table[{q, f[q]==g[q]},{q, -7 Pi, 7 Pi, 2 Pi}]

returns

{{-7 Pi,False},{-5 Pi,False},{-3 Pi,False},{-Pi,False},{Pi,False},{3 Pi,False},{5 Pi,False},{7 Pi,False}