diff options
| -rw-r--r-- | theories/Lists/List.v | 13 |
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. |