Add specification for iter_mut

[xldenis]

Adds a specification for [T]::iter_mut and the associated IterMut type.

One quirk is that where in RustHornBelt we modeled mutable iterators a sa sequence of borrows, I used a borrow of sequences here. They're equivalent of course but it corresponds to the specs I proved in preparation for RustVerify'22 (in 02_iter_mut.rs).

cc @jhjourdan