for n being Nat holds Polygon (0,n) = n * (2 - n) ;