let i, j be Nat; :: thesis: ( i > (i -' 1) + j implies j = 0 )
assume i > (i -' 1) + j ; :: thesis: j = 0
then (i - j) + j > (i -' 1) + j ;
then A2: i - j > i -' 1 by XREAL_1:6;
i - j >= 1
proof
assume A4: i - j < 1 ; :: thesis: contradiction
(i - j) + j > 0 + j by A2, XREAL_1:6;
then i - j is Nat by NAT_1:21;
hence contradiction by A2, A4, NAT_1:14; :: thesis: verum
end;
then i - j = i -' j by NAT_D:39;
hence j = 0 by A2, NAT_1:14, NAT_D:41; :: thesis: verum