Function seq_tracked_split_at 

pub proof fn seq_tracked_split_at<T>(tracked s: &mut Seq<T>, n: int) -> tracked result : Seq<T>

requires

0 <= n <= old(s).len(),

ensures

*final(s) == old(s)[..n],

result == old(s)[n..],

Splits a tracked sequence at position n, leaving [0, n) in s and returning [n, len).