Thm* a:, b:. q:, r:b. a = qb+r

To show this, we hold b   constant while we do induction over a   to prove

a:. q:, r:b. a = qb+r.

We use the true-for-less form of induction, assuming

a1:. a1<a  (q:, r:b. a1 = qb+r)

and attempt to show q:, r:b. a = qb+r.

If a<b then just use a for r, and 0 for q.

Otherwise, a-b   and a-b<a, so by our induction hyp,

a-b = qb+r for some q  , r  b,

so, a-b = qb+r, from which follows a = (q+1)b+r,

which show our goal to be satisfied using q+1 for q.

QED

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html