theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to
\exists s. r = (succ s) \land p + q == s.
intros. elim H; clear H q r; intros;
theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to
\exists s. r = (succ s) \land p + q == s.
intros. elim H; clear H q r; intros;