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