for n being Nat st n is odd holds
( 1 <= n & (n + 1) div 2 = (n + 1) / 2 )