--- a/Moment.thy	Sun Jan 31 18:15:13 2016 +0800
+++ b/Moment.thy	Mon Feb 01 20:56:39 2016 +0800
@@ -82,6 +82,12 @@
   using assms 
   by (simp add:moment_def rev_take, 
       metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)
+
+lemma moment_Suc_hd:
+  assumes "Suc i \<le> length s"
+  shows "hd (moment (Suc i) s) = s!(length s - Suc i)"
+  by (simp add:moment_def rev_take, 
+      subst hd_drop_conv_nth, insert assms, auto)
   
 lemma moment_plus:
   assumes "Suc i \<le> length s"