let n, n1, n2 be Nat; :: thesis: ( n1 + n <= n2 + 1 & n > 0 implies n1 <= n2 )
assume that
A1: n1 + n <= n2 + 1 and
A2: n > 0 ; :: thesis: n1 <= n2
1 + 0 <= n by A2, NAT_1:13;
hence n1 <= n2 by A1, XREAL_1:8; :: thesis: verum