let j, i be Nat; :: thesis: (j -' i) -' 1 = (j -' 1) -' i
(j -' i) -' 1 = j -' (i + 1) by NAT_2:32;
hence (j -' i) -' 1 = (j -' 1) -' i by NAT_2:32; :: thesis: verum