for n being Nat st n > 0 holds
card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1