-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.
- intros 2. elim q; clear q; intros;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst
- | clear H.
- lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- lapply linear eq_gen_succ_succ to H1 as H0.
- subst
- ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**)
+theorem nplus_inv_succ_2_3: \forall p,q,r.
+ (p + (succ q) == (succ r)) \to p + q == r.
+ intros.
+ lapply linear nplus_inv_succ_2 to H. decompose. subst. auto.