-theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
- intros 2. elim q; clear q;
- [ lapply linear nplus_gen_zero_2 to H as H0.
- subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- subst
- ]; auto new timeout=100.
+theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r.
+ intros. elim H; clear H q r; auto.
+qed.
+
+(* Corollaries *)
+
+theorem nplus_comm_1: \forall p1,q,r1. (p1 + q == r1) \to
+ \forall p2,r2. (p2 + q == r2) \to
+ \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1. subst
+ | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
+ lapply linear nplus_gen_succ_2 to H4. decompose. subst
+ ]; auto.