Issue with SPARK 2014

[Serge Robyns <serge.robyns@gmail.com>]

I'm trying to use SPARK on a little game, so far only one error remains and I've no clue on how to fix this.  I've been trying various approaches.
Here is the code snippet (hopefully complete enough).

      Count1      : Natural range 0 .. Number_Of_Columns;
      Count2      : Natural range 0 .. Number_Of_Columns;
      J           : Columns;
   begin
      Count1 := 0;
      if Column > Columns'First then
         for J in reverse Columns'First .. Columns'Pred (Column)
         loop
            pragma Loop_Variant ( Increases => Count1 );
            pragma Loop_Variant ( Decreases => J );
            pragma Loop_Invariant ( Count1 <= Integer (Columns'Pred (Column) - Columns'First) );
            exit when The_Board.Board (Row, J) /= Player;
            Count1 := Count1 + 1;
         end loop;
      end if;

Alternative:
      Count2 := 0;
      if Column < Columns'Last then
         for J in Columns'Succ (Column) .. Columns'Last
         loop
            pragma Loop_Variant ( Increases => Count2 );
            pragma Loop_Variant ( Increases => J );
            pragma Loop_Invariant ( Count2 < Number_Of_Columns );
            exit when The_Board.Board (Row, J) /= Player;
            Count2 := Count2 + 1;
         end loop;
      end if;

I get similar errors on both:
medium: loop invariant might fail after first iteration, requires Count1 <= Columns'pred - 1
medium: loop invariant might fail after first iteration, requires Count2 < Number_Of_Columns