Function vstd::seq_lib::lemma_seq_skip_build_commut

0 <= n <= s.len() ==> s.push(v).skip(n) =~= s.skip(n).push(v),

Pushing element v onto the end of sequence s and then skipping the first n elements is equivalent to skipping the first n elements of s and then pushing v onto the end.