def absValue(x) :
    """{ pre  x != 0
         post ans > 0
         return ans
    }"""
    if x < 0 :
        """{ 1.OK x != 0    premise
             2.OK x < 0     premise
        }"""
        ans = 0 - x
        """{ 1.OK x < 0         premise
             2.OK ans == 0 - x  premise
             3.OK ans > 0       algebra 1 2
        }"""
    else :
        """{ 1.OK x != 0       premise
             2.OK not(x < 0)   premise
             3.OK x >= 0       algebra 2
             4.OK x > 0        algebra 1 3
        }"""
        ans = x
        """{ 1.OK  ans == x   premise
             2.OK  x > 0      premise
             3.OK  ans > 0    subst 1 2
        }"""
    """{ 1.OK  ans > 0         premise   }"""  
    # that is, we proved (ans > 0  or  ans > 0), which is  ans > 0
    return ans
    # we proved the postcondition



m = readInt()
assert m <= 0
n = m - 1

"""{ 1.OK m <= 0                                premise
     2.OK n == m - 1                           premise
     3.OK m <= 0 and n == m - 1                 andi 1 2
     4.OK n-1 != 0                             algebra 1 2
     5.OK n-1 != 0 and (m <= 0 and n == m - 1)  andi 4 3
}"""
m = absValue(n-1)
"""{ 1.OK m > 0                                         premise  
     2.OK n-1 != 0 and (m_old <= 0 and n == m_old - 1)  premise
     3.OK m_old <= 0 and n == m_old - 1                 ande 2
     4.OK n - 1 <= 0                                       algebra 3
     5.OK m > 0  and  n - 1 <= 0                           andi 1 4
}"""