[P3-Float-to-Int Conversion] f64::to_int_unchecked

[Yenyun035]

Official Repo Tracking Issue

Tasks :

1. Write a proof for verifying the absence of arithmetic overflow/underflow and undefined behavior for the function.
2. Add proofs into a dedicated file, e.g. library/core/src/num/xx.rs
3. Please make sure not to modify other people's code, since we will be co-working on the same files. Avoid code conflicts as much as possible. Pull code every time a merge is made.

IMP: comment with the branch name you will be working on, with its link.

Ref: https://github.com/rajathkotyal/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md