Function lemma_seq_subrange_decreases 

pub broadcast proof fn lemma_seq_subrange_decreases<A>(s: Seq<A>, i: int, j: int)

requires

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

s[i..j].len() < s.len(),

ensures

#[trigger] (decreases_to!(s => s[i..j])),