let a be Nat; :: thesis: ( a <> 0 implies a - 1 >= 0 )
assume a <> 0 ; :: thesis: a - 1 >= 0
then a >= 1 by NAT_1:14;
then a - 1 >= 1 - 1 by XREAL_1:11;
hence a - 1 >= 0 ; :: thesis: verum