At:
div floor mod unique1
1.
a:
2.
n:
3.
q:
4.
r:
5.
a = qn+r
6.
r < n
7.
a = (a n)n+(a mod n)
8.
(a mod n) < n
q = (a n) & r = (a mod n)
By:
RepeatFor 2 (MoveToConcl -1)
THEN
GenConcl ((a n) = q')
THEN
Thin -1
THEN
GenConcl ((a mod n) = r')
THEN
Thin -1
THEN
Unfold `guard` 0
Generated subgoal:
a = q'
n+r' 
r' < n 
n)
