Function spec_ord_max 

pub open spec fn spec_ord_max<T: Ord>(x: T, y: T) -> T

{
    match y.cmp_spec(&x) {
        Ordering::Less => x,
        Ordering::Equal => y,
        Ordering::Greater => y,
    }
}

Returns x when y compares less than it, and returns y otherwise.