Add seq_add, seq_len_0

1 files changed, 8 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 8cfb626d2..abb1395b3 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1201,6 +1201,14 @@ Proof.
       rewrite Nat.add_succ_r; reflexivity. }
 Qed.
 
+Lemma seq_len_0 a : seq a 0 = nil. Proof. reflexivity. Qed.
+Lemma seq_add start a b : seq start (a + b) = seq start a ++ seq (start + a) b.
+Proof.
+  revert start b; induction a as [|a IHa]; cbn; intros start b.
+  { f_equal; omega. }
+  { rewrite IHa; do 3 f_equal; omega. }
+Qed.
+
 Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop),
   (forall x, In x l -> P x) <-> fold_right and True (map P l).
 Proof.