GNATprove: "overflow check might fail" SPARK 2018 error

I am developing two methods of exponentiating two numbers in ada and applying formal verification with spark and I can not solve these overflow errors, asking my teacher has told me that maybe I'm missing an invariant, but I can not determine what it would be, that's why I ask for help from someone who knows about the subject.

Thank you very much in advance, I await your answers.

Two methods are one by simple exponentiation and the other by binary exponentiation using binary expansion of the exponent.

These are the mistakes that Spark presents when doing Prove All:

practica.adb:20:17: medium: overflow check might fail (e.g. when A = 0 and r = 1)
practica.adb:40:33: medium: loop invariant might fail after first iteration, cannot prove r * (x ** y) = (M ** N (e.g. when M = 0 and N = 0 and r = 0 and x = 0 and y = 0)
practica.adb:44:20: medium: overflow check might fail (e.g. when x = 0)
practica.adb:47:20: medium: overflow check might fail (e.g. when r = 0 and x = 0)
practica.ads:8:19: medium: postcondition might fail, cannot prove power_simple'Result = (A ** B (e.g. when A = 0 and B = 2 and power_simple'Result = 0)
practica.ads:16:22: medium: postcondition might fail, cannot prove power_binary'Result = (M ** N (e.g. when M = 0 and N = 2 and power_binary'Result = 0)

my code in the .ads

package Practica with SPARK_Mode => On is

   -- Funcion que calcula la potenciacion de A elevado a B
   function power_simple (A : Natural; B : Natural) return Integer
     with Depends => (power_simple'Result => (A,B)), 
          Pre => B >= 0,
          Post => power_simple'Result = (A ** B)
                  and (if B = 0 then power_simple'Result = 1);


   -- Funcion que calcula mediante exponenciacion binaria, potencias de un numero dado
   function power_binary (M : Integer; N : Integer) return Integer
       with  Depends => (power_binary'Result => (M,N)),
             Pre => (M >= 0) and (N >= 0),
             Post => power_binary'Result = (M ** N)
             and (if N = 0 then power_binary'Result = 1);

end Practica;

my code in .adb

   -- Funcion que calcula la potenciacion de A elevado a B
   function  power_simple (A : Natural; B : Natural) return Integer is
      x : Integer := 0;
      r : Integer := 1;
   begin

      while x /= B loop
         pragma Loop_Invariant (0 <= x);
         pragma Loop_Invariant (x <= B);
         pragma Loop_Invariant (r = (A ** x));
         pragma Loop_Invariant (r >= 0);
         pragma Loop_Invariant ((if x = 0 then r /= 0));
         pragma Loop_Variant (Decreases => B - x);

         r := r * A;
         x := x + 1;

      end loop;

      if (B = 0) then r := 1; end if;
      if (B = 1) then r := A; end if;

      return r;
   end power_simple;


   --Funcion que calcula mediante exponenciacion binaria, potencias de un numero
   function power_binary(M : Integer; N : Integer) return Integer is
      x : Integer := M;
      y : Integer := N;
      r : Integer := 1;
   begin
      while y /= 0 loop
         pragma Loop_Invariant ((x >= 0) and (y >= 0));
         pragma Loop_Invariant (r * (x ** y) = (M ** N));
         pragma Loop_Variant (Decreases => y);

         if (y mod 2) = 0 then
            x := x * x;
            y := y / 2;
         else
            r := r * x;
            y := y - 1;
         end if;
      end loop;

      if (N = 0) then r := 1; end if;
      if (N = 1) then r := M; end if;

      return r;
   end power_binary;