Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

a:. n:. k:. a < n * k a n < k

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. a n < k