Stream: Coq users

Topic: element's existence in list


view this post on Zulip zeesha huq (Nov 01 2023 at 03:36):

Require Export List.
Require Export Arith.
Require Export Bool.

Lemma in_nm: forall a n m l ,
In n l->
In m l ->
(n<? length l) = true->
(m<? length l) = true.

view this post on Zulip Paolo Giarrusso (Nov 02 2023 at 11:06):

That statement is not true. Counterexample: l = [0; 1000], n = 0, m = 1000.

view this post on Zulip zeesha huq (Nov 04 2023 at 15:06):

(deleted)


Last updated: Jun 13 2024 at 19:02 UTC