I'm trying to construct an S5 proof of $\vdash\square(\square P\rightarrow\square Q)\vee\square(\square Q\rightarrow\square P)$.
I know that $\phi\vee\psi$ is equivalent to $\text{~}\phi\rightarrow\psi$, and so what I'm really trying to derive is $\text{~}\square(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$ (which is equivalent to $\lozenge\text{~}(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$), but I'm not sure what steps I'd have to take to reach this.
Your help would be appreciated.
(in S5 I have the axioms
$\square(\phi\rightarrow\psi)\rightarrow (\square\phi\rightarrow\square\psi)$
$\square\phi \rightarrow \phi$
$\lozenge\square\phi\rightarrow\square\phi$
as well as the rules modus ponens ($\phi$, $\phi\rightarrow\psi$ $\vdash \psi$) and necessitation ($\phi$ becomes $\square\phi$)).
EDIT: here are the approaches that I've considered so far:
As above, I know that what I need to prove is of the form:
$\lozenge\text{~}(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$
I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.
Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.
I could start by taking $(P\rightarrow Q) \rightarrow(\text{~}Q\rightarrow \text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(\square P\rightarrow\square Q) \rightarrow(\square \text{~}Q\rightarrow\square \text{~}P)$, but I can't see any obvious way to proceed from here.
I could also start by saying that $(\square P\rightarrow\square Q) \rightarrow(\text{~}\square Q\rightarrow\text{~}\square P)$, but again I see no obvious way to proceed because the negations make things more difficult.
I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.