let N, M, K be ExtNat; :: thesis:
assume A1: ( K <> 0 & N = M * K ) ; :: thesis:

per cases by Th3;

suppose N is Nat ; :: thesis:

then reconsider n = N as Nat ;

per cases ;

suppose M = 0 ; :: thesis:

hence M <= N ; :: thesis:

end;

suppose A2: M <> 0 ; :: thesis:

( M <> +infty & K <> +infty )

proof

assume ( M = +infty or K = +infty ) ; :: thesis:
then n = +infty by A1, A2, XXREAL_3:def 5;
hence contradiction ; :: thesis:

end;

then reconsider m = M, k = K as Nat by Th3;
n = m * k by A1;
hence M <= N by A1, NAT_1:24; :: thesis:

end;

end;

end;

suppose N = +infty ; :: thesis:

hence M <= N by XXREAL_0:3; :: thesis:

end;

end;