I want to find the smallest factor of a value with below specification 

```
procedure S_Factor (N : in out Positive; Factor : out Positive) with
         SPARK_Mode,
         Pre => N > 1,
         Post => (Factor > 1) and
         (N'Old / Factor = N) and
         (N'Old rem Factor = 0) and
         (for all J in 2 .. Factor - 1 => N'Old rem J /= 0)
       is

    begin
    ... 
    end S_Factor;

```

I wrote the body of the procedure try to cover all assert but always one of post condictions fail... 

```
procedure S_Factor (N : in out Positive; Factor : out Positive) with
     SPARK_Mode,
     Pre => N > 1,
     Post => (Factor > 1) and
     (N'Old / Factor = N) and
     (N'Old rem Factor = 0) and
     (for all J in 2 .. Factor - 1 => N'Old rem J /= 0)
   is

begin

      Factor := N;
      for J in 2 .. Factor loop
         if N rem J /= 0  then
         null;
         else
              Factor := J;
              N := N / Factor;

            exit;
               end if;

   end loop;

end S_Factor ;

```

What i am doing wrong? Can someone help me past through all assert from specification?