let k be Nat; :: thesis: ( 1 <= k implies (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1)) )
assume 1 <= k ; :: thesis: (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
then - ((Radix k) - (Radix (k -' 1))) = - (Radix (k -' 1)) by Lm2;
hence (- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1)) ; :: thesis: verum