Exercises 3.4 and 3.5

If there is a shorter solution to 3.4, then I'd like to know (and will add/substitute).
It's poor style to use Coq-generated names; they're somewhat fragile, and confusing to the reader who isn't replaying it in Coq.  You should `pose (...) as p`, or `pose (p := ...)`.