Move NI proof to dedicated file.

I started to work only on preservation of the invariant for now.
Definitions differ from the ones used for testing, although it should be easy to
see that the invariant is the same.