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

end;

end;