let x be Integer; :: thesis: for k being Nat st 2 <= k holds
( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )
let k be Nat; :: thesis: ( 2 <= k implies ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 ) )
assume k >= 2 ; :: thesis: ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )

per cases ( x < - (Radix (k -' 1)) or ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) or x >= Radix (k -' 1) ) ;

suppose x < - (Radix (k -' 1)) ; :: thesis: ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )

hence ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 ) by Def3; :: thesis: verum

end;

suppose ( - (Radix (k -' 1)) <= x & x < Radix (k -' 1) ) ; :: thesis: ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )

hence ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 ) by Def3; :: thesis: verum

end;

suppose x >= Radix (k -' 1) ; :: thesis: ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )

hence ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 ) by Def3; :: thesis: verum

end;

end;