There are two functions

f[x_] := Which[0 <= Mod[x, 2 \[Pi]] < \[Pi], Mod[x, \[Pi]], \[Pi] <= Mod[x, 2 \[Pi]] < 2 \[Pi], -Mod[x, \[Pi]] + \[Pi]]

and

g[x_] := \[Pi] (1 - (-1)^Quotient[x, \[Pi]])/2 + (-1)^Quotient[x, \[Pi]] Mod[x, \[Pi]]

They are equal, as can be seen from their graphs.
But how can this be proved with Wolfram tools?
In other words, how can Wolfram get g from f and vice versa?

Isn't it a challenge to the Wolfram expert to compare two fundamentally different definitions of the same mathematical entity and prove in a given system their equivalence?

As you can see from the name of the attached file, there is a third equivalent function: arccocos[x_]:=ArcCos[Cos[x]]. So the task becomes more complicated. We need to justify the equality of the three functions in Wolfram.