[Spark] Proving GCD

["Frédéric Praca" <frederic.praca@free.fr>]

Hi guys,
sorry for the first message, I clicked on the wrong button :D

I'm trying to train myself on Spark and I tried to see if a simple 
function like GCD could be proved.

I created the following :

GCD_Package is

   pragma SPARK_Mode;
   pragma Assertion_Policy(Check);
   
   function gcd (A : Natural; B : Positive) return Natural
     with
       Global => null,
       Depends => (gcd'Result => (A,B)),
       Post => gcd'Result <= A and A mod gcd'Result = 0 and B mod
       gcd'Result = 0 ;

end GCD_Package;

package body GCD_Package is

   pragma SPARK_Mode;

   function gcd (A : Natural; B : Positive) return Natural is
      Value : Natural;
      Temp : Natural; Local_B : Natural := B;
      Local_A : Natural := A;
   begin
      if A = 0 then
         value := B;
      else
         while Local_B > 0 loop
            pragma Loop_Variant (Decreases => Local_B);
            Temp := Local_B;
            Local_B := Local_A mod Local_B;
            Local_A := Temp;
         end loop;
         value := Local_A;
      end if;
      
      return value;
   end Gcd;

end GCD_Package;

The answer is always "postcondition might fail" and I don't know what to 
do. 
Do you have an idea on how to discharge all VCs and thus prove this code ?

Thanks
Fred