mathlib3

ab27827f - closer to partial summation nat