Definition:
Subtraction: if
.
Division: if
.
Theorem:
8.
,
.
proof of 8: By F3 ,
;
By F5 ,
;
By F3 ,
;
By Thm P1,
.
9.
s.t.
;
s.t.
.
proof of 9: By F3 ,
is not equal to
.
10.
.
11.
.
12.
.
proof of 12: <= : By P8 , if
, then
;
By P8 , if
, then
.
=> : Assume
, if a = 0 we are done;
Otherwise , by P8 ,
is not equal to
and we have
;
by cancellation (P2) ,
.
.
proof: By F5 ,
Theorem :
s.t.
1.
;
2. For every
,
;
3. For every
,
.
iota(2) = iota(1+1) = iota(1) + iota(1) = 1 + 1;
iota(3) = iota(2+1) = iota(2) + iota(1) = iota(2) + 1;
......
In F2 ,