diff -r 83ba2d8c859a -r 2aa37de77f31 Moment.thy
--- a/Moment.thy	Thu Jan 14 00:55:54 2016 +0800
+++ b/Moment.thy	Thu Jan 14 03:29:22 2016 +0000
@@ -8,20 +8,6 @@
 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
 value "moment 2 [5, 4, 3, 2, 1, 0::int]"
 
-(*
-lemma length_moment_le:
-  assumes le_k: "k \<le> length s"
-  shows "length (moment k s) = k"
-using le_k unfolding moment_def by auto
-*)
-
-(*
-lemma length_moment_ge:
-  assumes le_k: "length s \<le> k"
-  shows "length (moment k s) = (length s)"
-using assms unfolding moment_def by simp
-*)
-
 lemma moment_app [simp]:
   assumes ile: "i \<le> length s"
   shows "moment i (s' @ s) = moment i s"