Function spec_expect_err 

pub open spec fn spec_expect_err<T: Debug, E>(result: Result<T, E>, msg: &str) -> E

recommends

result is Err,

{ result->Err_0 }

Returns the error value when result is Err.