Results 4 issues of LevitatingLion

I would like to make the fact that certain conditions are verified to always hold available to the optimizer. With this, things like bounds checks or `unwrap`s that are verified...

enhancement

It would be great if Creusot provided a `cfg(creusot)` when compiling under `cargo creusot`. This would remove the need for the `contracts` feature in `creusot-contracts`, since the Creusot-specific code could...

Similar to #504, but now for `Result`.

This is the second half of PR #504. Also adds `ok_or` and `ok_or_else`, which require some basic operations on `Result`s to be specified before the test can be verified.