( 0 < PI / 4 & PI / 4 < PI ) by Lm9, XXREAL_1:4;
then arccot 1 = PI / 4 by Th16, Th34;
hence ( arccot 1 = PI / 4 & arccot . 1 = PI / 4 ) ; :: thesis: verum