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