per cases ( not n is zero or n is zero ) ;

suppose A: not n is zero ; :: thesis: n -' 1 is natural

then n >= 1 by NAT_1:14;
then n -' 1 = n - 1 by XREAL_0:def 2;
hence n -' 1 is natural by A; :: thesis: verum

end;

suppose n is zero ; :: thesis: n -' 1 is natural

then n - 1 < 0 ;
hence n -' 1 is natural by XREAL_0:def 2; :: thesis: verum

end;

end;