integration of statements for seq

1 files changed, 13 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index fae766d6b9..3e681b7d05 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2286,6 +2286,11 @@ Section NatSeq.
       | S len => start :: seq (S start) len
     end.
 
+  Lemma cons_seq : forall len start, start :: seq (S start) len = seq start (S len).
+  Proof.
+    reflexivity.
+  Qed.
+
   Lemma seq_length : forall len start, length (seq start len) = len.
   Proof.
     induction len; simpl; auto.
@@ -2336,6 +2341,14 @@ Section NatSeq.
     - now rewrite Nat.add_succ_r, IHlen.
   Qed.
 
+  Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len].
+  Proof.
+   intros len start.
+   change [start + len] with (seq (start + len) 1).
+   rewrite <- seq_app.
+   rewrite <- plus_n_Sm, <- plus_n_O; reflexivity.
+  Qed.
+
 End NatSeq.
 
 Section Exists_Forall.