Level:
Lib
Thy
Top
:
1
Hypotheses:
E :
n :
k :
EquivRel(
;x,y.
(x E y))
(n E k)
Conclusion:
Min{ x | xEn } = Min{ x | xEk }
Applied Tactic:
Unfold `min_el` 0
Generated subgoals:
1
. MinArg(E n : {0..n
}) = MinArg(E k : {0..k
})
;x,y.
(x E y))(n E k)
Min{ x | xEn } = Min{ x | xEk }
}) = MinArg(E k : {0..k})