theorem Th56: :: SIN_COS9:56

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