Documentation improvements

[utaal]

This contains a list of documentation improvements that we'd like to do.

[utaal]

@matthias-brun notes that:

let mut i = 8;
while i < 4
    invariant i < 8
{ }

gives "invariant not satisfied before loop", and asks "is there a reason I don't get to assume the loop condition for that proof?".

This is because the invariant would be assumed true at loop exit, but it isn't.

@matthias-brun suggests adding these explanations to the doc.

@utaal: Also, one does not get the invariant on break because we are not re-establishing the invariant on break (unless it's an invariant_ensures). [This is already documented.]