theorem :: NUMPOLY1:66

for n being non zero Nat holds (Triangle n) + (Triangle (n -' 1)) = (((1 + (2 * n)) - 1) * n) / 2