Function take_postcondition 

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

requires

i.obeys_prophetic_iter_laws(),

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

ensures

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

take_iter(r) == i,

take_count(r) == n,

IteratorSpec::will_return_none(&r) <==> i.will_return_none() || i.remaining().len() >= n,

IteratorSpec::decrease(&r) is Some,