Level:
Lib
Thy
Top
:
1
Hypotheses:
None
Conclusion:
n:
.
f:
n
. Bij(
n;
;f)
Applied Tactic:
With
2
(D 0) THENW Auto
Generated subgoals:
1
.
f:
2
. Bij(
2;
;f)
n:
. f:n 
. Bij(n;;f)
2
(D 0) THENW Autof:2 . Bij(2;;f)