Step
*
of Lemma
imax_ge_left
a,b:
.
(imax(a;b)
a
)
BY
{
RepeatFor
2
((D
0
THENA
Auto))
}
1
1.
a
:
@i
2.
b
:
@i
imax(a;b)
a
Latex:
\mforall{}a,b:\mBbbZ{}. (imax(a;b) \mgeq{} a )
By
RepeatFor 2 ((D 0 THENA Auto))
Home
Index
a,b:
. (imax(a;b) 
a )@i@i
imax(a;b) a