let a, b be Nat; :: thesis: ( b = 0 or b + a in seq (a,b) )

assume b <> 0 ; :: thesis: b + a in seq (a,b)

then ex c being Nat st b = c + 1 by NAT_1:6;

then 1 <= b by NAT_1:11;

then ( b + a is Element of NAT & 1 + a <= b + a ) by ORDINAL1:def 12, XREAL_1:6;

hence b + a in seq (a,b) ; :: thesis: verum

assume b <> 0 ; :: thesis: b + a in seq (a,b)

then ex c being Nat st b = c + 1 by NAT_1:6;

then 1 <= b by NAT_1:11;

then ( b + a is Element of NAT & 1 + a <= b + a ) by ORDINAL1:def 12, XREAL_1:6;

hence b + a in seq (a,b) ; :: thesis: verum