I think we want empty lines before and after any nontrivial definitions (i.e., anything that has types, and/or is not `Definition Book_n_m := @constant.`)