A1: PI / 2 < PI / 1 by XREAL_1:76;
arccot 0 = PI / 2 by A1, Th36, Th42;
hence ( arccot 0 = PI / 2 & arccot . 0 = PI / 2 ) ; :: thesis: verum