`BookProof.ChapterF4.mgRun_sum` (k : ℕ) (xs : List ι) : (∑ a, (mgRun k xs).1 a) + (k + 1) * (mgRun k xs).2 = xs.length

Initializing...

`BookProof.ChapterF4.mgRun_sum` (k : ℕ) (xs : List ι) : (∑ a, (mgRun k xs).1 a) + (k + 1) * (mgRun k xs).2 = xs.length · Prove2Me