Add imports for *-mono-<= exercise

[negatratoron]

Closes #1079

[wadler]

Thanks.

*-comm should not be imported, not least because it is one of the later exercises.

[negatratoron]

Isn't *-comm an earlier exercise, in Induction?

I had added it because I used it in the proof, and figured it was reasonable to have that in the imports since +-comm is used in the example proof of +-mono-<=.

I did remove it from the PR, but IMO it should be present, even though it serves as a hint if the reader looks closely at the imports.

[negatratoron]

While I have you here, thanks for all your effort on this book by the way! It's really well-written, and I also appreciate all the talks you've given that I can watch on youtube.

[negatratoron]

@wadler Just a reminder, I made the change and I'm perfectly happy with it, go ahead and merge if you're ready