qed.
theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
\exists s. p = succ s \land (s + q == r) \lor
q = succ s \land p + s == r.
qed.
theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to
\exists s. p = succ s \land (s + q == r) \lor
q = succ s \land p + s == r.