Level: Lib Thy Top: 1
Hypotheses:

  1. a :

  2. n :

  3. k :

  4. a < n * k

Conclusion:

a n < k

Applied Tactic: Decide a n k THENW Auto
Generated subgoals:

1. a n < k

2. a n < k