b - 1 < 1 - 1 ;
hence [\b/] is zero by INT_1:def 6; :: thesis: verum