No specification for `OrdSpec::cmp_spec` for `int`

[jaylorch]

I was surprised to learn that you can talk about cmp_spec for int, but it doesn't have any specs about it so it's meaningless. (I learned this when Copilot scolded me for using it in a spec.) For instance, you can't even know that 3 is less than 4:

proof fn int_cmp_spec()
    ensures
        OrdSpec::cmp_spec(&3int, &4int) is Less,
{
}

gives

error: postcondition not satisfied
  --> src\main.rs:36:9
   |
34 | proof fn int_cmp_spec()
   |       ----------------- at the end of the function body
35 |     ensures
36 |         OrdSpec::cmp_spec(&3int, &4int) is Less,
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ failed this postcondition