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