let n, a be non zero Nat; :: thesis: 1 <= a * n
0 + 1 <= a * n by NAT_1:13;
hence 1 <= a * n ; :: thesis: verum