How to use Hoare Logic to Prove this Assertion

Question

Given this assertion in Hoare Logic:

\begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\ &\mathbf{\{s == p * (p + 1) / 2\}} \end{align}

How to prove this using the rules of Hoare Logic. I am not sure where to really begin, I only currently understand (most) of the meaning of the axioms, but not what is required for a proof.