Step
*
of Lemma
bnot_of_lt_int
∀[i,j:ℤ]. ¬
b
i <z j = j ≤z i
BY
{ Auto }
Latex:
Latex:
\mforall{}[i,j:\mBbbZ{}]. \mneg{}\msubb{}i <z j = j \mleq{}z i
By
Latex:
Auto
Home
Index