Is this expected behavior or not

[Anh Vo <anhvofrcaus@gmail.com>]

I have read ARM section 3.2.4, Subtype Predicates, I did not see any rules prohibiting from using attribute 'Succ as contained in the code nipet below. I would expect Prime'Succ (3) return 5 for next prime number. However, 4 is returned instead. Is this a correct behavior?

pragma Assertion_Policy (Check);
with Ada.Text_Io;
with Ada.Exceptions; use Ada;

procedure Predicates_Test is
   use Text_Io;

   subtype Prime is Natural range 1 .. 1000
      with Dynamic_Predicate =>
      (case Prime is
         when 1 => False,
         when 2 => True,
         when others => Prime mod 2 /= 0 and then
                        (for all K in 3 .. Prime - 1 => Prime mod K /= 0));

   Current_Prime_Number : constant Natural := 3;
   Next_Prime_Number : constant Natural := 5;

begin
   Put_Line ("Predicates_Test starts");

   if Prime'Succ (Current_Prime_Number) = Next_Prime_Number then
      Put_Line ("The next prime number matches expectation");
   else
      Put_Line (Prime'Succ(Current_Prime_Number)'Img &
                                              " is not an expected number");
   end if;

   Put_Line ("Predicates_Test ends");
exception
   when Err : others =>
      Put_Line ("Houston we have a problem: " &
                                       Exceptions.Exception_Information(Err));
end Predicates_Test;