mathlib3

545ae2f7 - Improved partial summation proof