FindEquationalProof does not know by default the rules of arithmetic, so you need to provide them as additional axioms. In this case only the (abelian) group of the addition operation is needed:
additiveGroup = AxiomaticTheory[{"AbelianGroupAxioms", "Multiplication" -> plus, "Identity" -> zero, "Inverse" -> minus}]
Then you can obtain a proof of your case with
FindEquationalProof[plus[p, q] == m, {additiveGroup, {plus[x, p] == z, plus[x, minus[q]] == y, plus[z, minus[y]] == m}}]