let n be Nat; :: thesis: ( n is odd implies ( 1 <= n & (n + 1) div 2 = (n + 1) / 2 ) )
assume L010: n is odd ; :: thesis: ( 1 <= n & (n + 1) div 2 = (n + 1) / 2 )
then 0 < 0 + n ;
hence 1 <= n by NAT_1:19; :: thesis: (n + 1) div 2 = (n + 1) / 2
thus (n + 1) div 2 = (n + 1) / 2 by L010, NAT_6:4; :: thesis: verum