add another loop invariant and remove additional assertions
add remaining loop invariants adapt proofs
remove another admit