-variant nplus_gen_succ_3_alt: \forall p,q,r. NPlus p q (succ r) \to
- \exists s. p = succ s \land NPlus s q r \lor
- q = succ s \land NPlus p s r.
+variant nplus_gen_succ_3_alt: \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.