Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
f:
.
n:
. f MinArg(f : {0..n
}) = f n
Applied Tactic:
Unfold `min_arg` 0
Generated subgoals:
1
.
f:
.
n:
. f (n - MinAr(f;n;n)) = f n
f:
. n:. f MinArg(f : {0..n
}) = f nf: . n:. f (n - MinAr(f;n;n)) = f n