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