pub broadcast proof fn lemma_seq_skip_index2<A>(s: Seq<A>, n: int, k: int)Expand description
ensures
0 <= n <= k < s.len() ==> (#[trigger] s[n..])[k - n] == #[trigger] s[k],If k is a valid index between n (inclusive) and the length of sequence s (exclusive),
then the k-nth element of the sequence s[n..] is the same as the kth element of the
original sequence s.