theorem NF992: :: BINPACK1:1

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