let i, j be Nat; :: thesis: ( i <= j & j <= i + 3 & not j = i & not j = i + 1 & not j = i + 2 implies j = i + 3 )
assume A0: ( i <= j & j <= i + 3 ) ; :: thesis: ( j = i or j = i + 1 or j = i + 2 or j = i + 3 )

now :: thesis: ( ( j <= i + 1 & ( j = i or j = i + 1 ) ) or ( j > i + 1 & ( j = i + 2 or j = i + 3 ) ) )

per cases ( j <= i + 1 or j > i + 1 ) ;

case j <= i + 1 ; :: thesis: ( j = i or j = i + 1 )

hence ( j = i or j = i + 1 ) by A0, NAT_1:9; :: thesis: verum

end;

case j > i + 1 ; :: thesis: ( j = i + 2 or j = i + 3 )

then (i + 1) + 1 <= j by NAT_1:13;
then ( j = i + 2 or j = (i + 2) + 1 ) by A0, NAT_1:9;
hence ( j = i + 2 or j = i + 3 ) ; :: thesis: verum

end;

end;

end;

hence ( j = i or j = i + 1 or j = i + 2 or j = i + 3 ) ; :: thesis: verum