let n, i be natural Number ; :: thesis: ( n -' i = 0 implies n <= i )
assume A1: n -' i = 0 ; :: thesis: n <= i
assume i < n ; :: thesis: contradiction
then i + 1 <= n by NAT_1:13;
then (i + 1) - i <= n - i by XREAL_1:9;
hence contradiction by A1, XREAL_0:def 2; :: thesis: verum