for i, n being Nat st i <= n holds
(n - i) + 1 is Element of NAT