for n being Nat holds Reci-TSq . n >= 0