Function skip_postcondition 

pub broadcast proof fn skip_postcondition<I: IteratorSpec>(i: I, n: usize, r: Skip<I>)

requires

i.obeys_prophetic_iter_laws(),

#[trigger] skip_post(i, n, r),

ensures

IteratorSpec::remaining(&r)
    == if i.remaining().len() < n { Seq::empty() } else { i.remaining()[n..] },

skip_iter(r) == i,

skip_init_n(r) == n,

IteratorSpec::will_return_none(&r) <==> i.will_return_none(),

IteratorSpec::decrease(&r) is Some == i.decrease() is Some,