Function vstd::relations::lemma_new_first_element_still_sorted_by

source · 
pub proof fn lemma_new_first_element_still_sorted_by<T>(
    x: T,
    s: Seq<T>,
    less_than: FnSpec<(T, T), bool>
)
Expand description
requires
sorted_by(s, less_than),
s.len() == 0 || less_than(x, s[0]),
total_ordering(less_than),
ensures
sorted_by(seq![x].add(s), less_than),