1 * n <= k * n by NAT_1:4, INT_1:74;
hence n <= k * n ; :: according to EC_PF_2:def 1 :: thesis: verum