Level: Lib Thy Top: 1 1
Hypotheses:

  1. P :

  2. n :

  3. k:{n...}. P k (i:k. P i)

  4. m :

  5. P m

  6. m < n

Conclusion:

m:n. P m

Applied Tactic: With m (D 0) THEN Auto
Generated subgoals:

None