--- a/prio/Moment.thy	Tue Apr 17 15:55:37 2012 +0000
+++ b/prio/Moment.thy	Fri Apr 20 11:27:49 2012 +0000
@@ -770,4 +770,14 @@
   thus ?thesis by (simp add:restm_def)
 qed
 
+lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)"
+proof -
+  from moment_plus_split [of i "length s" "t@s"]
+  have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"
+    by auto
+  with app_moment_restm[of t s]
+  have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp
+  with moment_app show ?thesis by auto
+qed
+
 end
\ No newline at end of file