Function vstd::seq_lib::lemma_seq_skip_len

source · 
pub proof fn lemma_seq_skip_len<A>(s: Seq<A>, n: int)
Expand description
ensures
0 <= n <= s.len() ==> s.skip(n).len() == s.len() - n,

Skipping the first n elements of a sequence gives a sequence of length n less than the original sequence’s length.