theorem Th22: :: SIN_COS9:22

rng (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(- 1),1.]