From 8d8a0f0ae1d68b96726d395e32f96d8aa6c3d316 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 18:32:37 +0100
Subject: [PATCH] rename seq_S_end_app -> seq_S_snoc
---
theories/list_numbers.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index f4116df1..4a8b2af4 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -67,7 +67,7 @@ Section seq.
Qed.
Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
- Lemma seq_S_end_app j n : seq j (S n) = seq j n ++ [j + n].
+ Lemma seq_S_snoc j n : seq j (S n) = seq j n ++ [j + n].
Proof.
revert j. induction n as [|n IH]; intros j; simpl in *; f_equal; [done |].
by rewrite IH, Nat.add_succ_r.
--
GitLab