Some remark, or maybe qestion about simple example on whiteboard... since we always entering that loop with x increment we should get postcondition of x > 0 strictly... why do all reasoning with intervals leads to x in [0, +inf] interval?