Function lemma_seq_subrange_len 

pub broadcast proof fn lemma_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)

requires

0 <= j <= k <= s.len(),

ensures

#[trigger] s[j..k].len() == k - j,