Level: Lib Thy Top: 1
Hypotheses:

  1. n :

Conclusion:

(n)!

Applied Tactic: NatInd 1 THENA Auto
Generated subgoals:

1. (0)!

2. (n)!