+theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 →
+ ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3.
+ intros 4; elim H; clear H p2 r1;
+ [ lapply linear nplus_inv_zero_1 to H2. destruct.
+ lapply nplus_mono to H1, H3. destruct. autobatch
+ | lapply linear nplus_inv_succ_1 to H3. decompose. destruct.
+ lapply linear nplus_inv_succ_1 to H4. decompose. destruct.
+ lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch
+ ].
+qed.
+