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

per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: M <= N

then reconsider n = N as Nat ;

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

suppose M = 0 ; :: thesis: M <= N

hence M <= N ; :: thesis: verum

end;

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

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

proof

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

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: verum

end;

end;

end;

suppose N = +infty ; :: thesis: M <= N

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

end;

end;