reconsider k = (Im a) - 1 as negative Real ;
k - 1 < 0 - 1 by XREAL_1:9;
then - (k - 1) > - (- 1) by XREAL_1:24;
then |.(k - 1).| > 1 by ABSVALUE:def 1;
hence (Im a) - 2 is heavy ; :: thesis: verum