Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. k :

  3. 0 < k

Conclusion:

(nk) = n * (nk - 1)

Applied Tactic: RecCaseSplit `exp` THEN Auto
Generated subgoals:

None