diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 8 |
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. |