int
2
Sections
StandardLIB
Doc
Def
Div(a;n;q) == n
q
a < n
(q+1)
is mentioned by
Thm*
a:
, n:
, p,q:
. Div(a;n;p)
Div(a;n;q)
p = q
[div_unique]
Thm*
a:
, n:
.
q:
. Div(a;n;q) & (a
n) = q
[div_elim]
Thm*
a:
, n:
. Div(a;n;a
n)
[div_fun_sat_div_nrel]
Def
Rem(a;n;r) ==
q:
. Div(a;n;q) & q
n+r = a
[rem_nrel]
Try larger context:
StandardLIB
int
2
Sections
StandardLIB
Doc