fix: missing decrement of j in snapshots example.

[isan-Ethen]

The example on the snapshots page of the Creusot User Guide is an insertion sort, but the decrement of j inside the while loop is missing.

[xldenis]

Thanks! if you don't mind I'm going to add a proof for this as well.

[isan-Ethen]

Thank you for your response! Of course I don't mind.

[xldenis]

I've added insertion_sort.rs with a proof, and adjusted the documentation to highlight the usage of snapshot! without getting lost in the details of the proof.

[isan-Ethen]

Sorry, is there any problem with my pull request?

[xldenis]

Nope! only with my proof.

[isan-Ethen]

Ah, I see. I was worried if I had made any mistakes.

[xldenis]

there we go, this should work. It turns out we merged #1005 just before I pushed my commit which bumped the version of Alt-Ergo causing the proof to be considered out of date.