per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: n / q is natural

hence n / q is natural ; :: thesis: verum

end;

suppose A1: n <> 0 ; :: thesis: n / q is natural

consider k being Integer such that
A2: q * k = n by Def2, INT_1:def 3;
0 <= k by A2, A1;
then A3: k in NAT by INT_1:3;
n / q = (q * k) * (q ") by A2, XCMPLX_0:def 9
.= k * (q * (q "))
.= k * 1 by A1, XCMPLX_0:def 7 ;
hence n / q is natural by A3; :: thesis: verum

end;

end;