(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
rem
rem
to
rem
1
1.
a:
2.
n:
((a rem n) rem n) = (a rem n)
By:
RWNth 1 (LemmaC
Thm*
a:
, n:
. a < n
(a rem n) = a) 0
Generated subgoals:
1
(a rem n) < n
2
(a rem n) = (a rem n)
About:
(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
(a rem n) < n (a rem n) = (a rem n)
((a rem n) rem n) = (a rem n)
a:, n:. a < n 
(a rem n) = a)
0 (a rem n) < n (a rem n) = (a rem n)
