How can I use destruct given the constraint I have for index range of a list?

Using Coq
1

Hi,

I’m trying to prove that for a list of bytes a, all bytes are x01 from index 2 to (n-m-2), where n is the length of a:

(forall (i : nat), ((i >= 2) /\ (i < ((n - m) - 1))) -> ((nth_error a i) = (Some x01)))

And in the context I do have this:

H : nth_error a ?j =
      nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j

So, after intros i i_range. I have:

i : nat
i_range : is_true (1 < i) /\ is_true (i < n - m - 1)
H : nth_error a ?j =
      nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list  ?j
______________________________________(1/1)
nth_error a i = Some x01

Is this a right approach to destruct RHS of H to eliminate the first two bytes and the last m bytes? If so, how can I do that with respect to i_range? Let me know if my proof strategy is flawed.

Thanks in advance for any suggestion.

2

This question has been answered here: