diff options
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8260058f1..8823a177e 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -633,11 +633,6 @@ Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs). reflexivity. Qed. -Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat. -Proof. - destruct a; omega. -Qed. - Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs). Proof. auto. @@ -976,6 +971,14 @@ Qed. Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn. +Lemma sum_firstn_0 : forall xs, + sum_firstn xs 0 = 0%Z. +Proof. + destruct xs; reflexivity. +Qed. + +Hint Rewrite @sum_firstn_0 : simpl_sum_firstn. + Lemma sum_firstn_succ : forall l i x, nth_error l i = Some x -> sum_firstn l (S i) = (x + sum_firstn l i)%Z. |