let i, k be Nat; :: thesis: ( i + 1 <= k implies 1 <= k -' i )
assume i + 1 <= k ; :: thesis: 1 <= k -' i
then (i + 1) -' i <= k -' i by NAT_D:42;
hence 1 <= k -' i by NAT_D:34; :: thesis: verum