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.