theorem :: COMPTRIG:61

for a being Real st 0 <= a & a < 2 * PI & cos a = 1 holds
a = 0