Level:
Lib
Thy
Top
:
1
2
Hypotheses:
P :
n :
k:{n...}. P k
(
i:
k. P i)
m :
P m
(m < n)
Conclusion:
m:
n. P m
Applied Tactic:
Assert
i:
((m - n) + 2).
l:
((m - i) + 1). P l
Generated subgoals:
1
.
i:
((m - n) + 2).
l:
((m - i) + 1). P l
2
.
m:
n. P m
k:{n...}. P k 
(
i:k. P i)
(m < n)
m:n. P m
i:((m - n) + 2). l:((m - i) + 1). P l
i:((m - n) + 2). l:((m - i) + 1). P lm:n. P m