Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n,k:
. 0 < k
(n
k) = n * (n
k - 1)
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. (n
k) = n * (n
k - 1)
n,k:
. 0 < k 
(n
k) = n * (nk - 1)k) = n * (nk - 1)