+(* Basic inversion properties ***********************************************)
+
+lemma plus_inv_dx: ∀ri,rs,ti,ts,c1,c2. 〈ri,rs,ti,ts〉 = c1 + c2 →
+ ∃∃ri1,rs1,ti1,ts1,ri2,rs2,ti2,ts2.
+ ri1+ri2 = ri & rs1+rs2 = rs & ti1+ti2 = ti & ts1+ts2 = ts &
+ 〈ri1,rs1,ti1,ts1〉 = c1 & 〈ri2,rs2,ti2,ts2〉 = c2.
+#ri #rs #ti #ts * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
+<plus_rew #H destruct /2 width=14 by ex6_8_intro/
+qed-.
+
+(* Main Properties **********************************************************)
+
+theorem plus_assoc: associative … plus.
+* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 * #ri3 #rs3 #ti3 #ts3
+<plus_rew //