let k be Nat; :: thesis: ( 2 <= k implies SDSub_Add_Carry 0 ,k = 0 )
assume k >= 2 ; :: thesis: SDSub_Add_Carry 0 ,k = 0
set x = 0 ;
A1: Radix (k -' 1) <> 0 by POWER:39;
- (Radix (k -' 1)) <= 0 - 0 ;
hence SDSub_Add_Carry 0 ,k = 0 by A1, Def3; :: thesis: verum