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