for n being Nat holds len ((Newton_Coeff n) | n) = n