Put `Array' and `rects' in definition environments

- so they can be referenced more visible from elsewhere
Finish theorem proof

- MaxRectangle is solvable in linear time