Function spec_ord_min 

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

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

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