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

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