PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
rem
quo
unique
1
1
1
1
1.
n:
2.
r1:
n
3.
r2:
n
4.
q1:
5.
q2:
6.
r1+q1
n = r2+q2
n
7.
(r1 rem n) = (r2 rem n)
r1 = r2
By:
RWH (LemmaC
Thm*
a:
, n:
. a < n
(a rem n) = a) 7
Generated subgoals:
None
About:
nn
n = r2+q2n
r1 = r2
a:, n:. a < n 
(a rem n) = a)
7
