The proofs are neither short nor nice, but at least they compile
fast (4 sec for the whole file) and the statements look like
they would look like on paper.