let a be natural Number ; :: thesis: ( a <> 0 implies a - 1 >= 0 )
assume a <> 0 ; :: thesis: a - 1 >= 0
then a - 1 >= 1 - 1 by XREAL_1:9, NAT_1:14;
hence a - 1 >= 0 ; :: thesis: verum