for i1, i2 being Integer st i2 <= i1 holds
i1 - i2 in NAT