Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
E:
.
n:
. Min{ x | xEn }
Applied Tactic:
Unfold `min_el` 0 THEN Auto
Generated subgoals:
None
E:
. n:. Min{ x | xEn } 