for n being Nat holds Polygon (1,n) = (n * (3 - n)) / 2 ;