let
k
be
Nat
;
:: thesis:
SDSub_Add_Carry
(
0
,
k
)
=
0
set
x
=
0
;
(
Radix
(
k
'
1
)
<>
0
&

(
Radix
(
k
'
1
)
)
<=
0

0
)
by
POWER:34
;
hence
SDSub_Add_Carry
(
0
,
k
)
=
0
by
Def3
;
:: thesis:
verum