Order-type of models of PA

I'd like to do a bit of work on the proof that every non-standard model of PA has order-type N+ZxQ. Some of the proofs are quite sketchy and I'd like to add a bit more detail, but I also wondered about going beyond this and changing the overall presentation to be a bit more precise about what's being proved, and perhaps restructuring the sequence of propositions a bit.

Does this sound reasonable? My thought here is that this is a fairly advanced result by Open Logic standards, and as such if it's being taught at all then it should be ok if it's presented in a somewhat more technical manner. I don't want to lose the intuitiveness of the current presentation (and in fact it would actually be nice to add more diagrams, as I think this is a result which is particularly amenable to them) but when I was teaching this myself I found it wasn't always clear what the exact statement of a given result was (e.g. in the proposition that introduces the idea of a block).

Start with the current presentation of the proof that every non-standard model of PA has order-type N+ZxQ, especially the proposition introducing blocks. Clarify the exact statement of each result, expand the sketchy proofs, and assess where diagrams and a revised proposition sequence would improve the exposition. Done means the advanced result is technically precise without losing its intuitive presentation.