(Im a) - 1 <= |.a.| - 1 by COMPLEX1:55, XREAL_1:9;
hence not (Im a) - 1 is positive ; :: thesis: verum