Create more examples of Micro Rust and its verification

The `Micro_Rust_Examples` session contains some explanatory material for working with `crush`, our weakest-precondition reasoning tactic, and the Micro Rust language, but could do with some more, polished examples. Some suggested verification projects that could serve as nice examples of our framework include:

- In-place sorting of an array, for example via quicksort,
- Manipulating tree data-structures,
- Smaller, more self-contained examples, for example a proof of correctness of an iterative implementation of the Fibonacci function, or similar.

Start by reading the existing `Micro_Rust_Examples` session and its material on `crush` and Micro Rust. Choose one suggested project, such as iterative Fibonacci, in-place sorting, or tree manipulation, and add a polished explanatory example with its verification; done means the example is complete and integrated into that session.

Written by the indexing model from the issue text.