bool
1
Doc
Def
i
z j ==
j < z i
Thm*
assert_of_le_int
Thm*
bnot_of_le_int