Am I overlooking something that would let Mathematica recognize that
Assuming[0 <= a < 2 R,
FullSimplify[ArcTan[Sqrt[a/(2 R - a)]] - ArcCos[1 - a/R]]]
is
-1/2 ArcCos[1 - a/R]
By adding what seem to be redundant assertions like 2*R - a > 0 && a > 0 && R > 0 I can get it to push the ArcTan into ArcSin, but not get it to - 1/2 ArcCos
