Slight improvements and more lemmas.

Got rid of `firstorder`, minor stylistic changes, and added lemmas that
connect min/max with arithmetic.