The antidiagonal of a natural number n is
the finset of pairs (i,j) such that i+j = n.
i+j = n
A pair (i,j) is contained in the antidiagonal of n if and only if i+j=n.
The cardinality of the antidiagonal of n is n+1.
The antidiagonal of 0 is the list [(0,0)]
A point in the antidiagonal is determined by its first co-ordinate.