let
k
,
n
be
Nat
;
:: thesis:
(
k
>=
1 implies
n
<=
k
*
n
)
assume
k
>=
1 ;
:: thesis:
n
<=
k
*
n
then
1
*
n
<=
k
*
n
by
NAT_1:4
;
hence
n
<=
k
*
n
;
:: thesis:
verum