with Ada.Numerics.Big_Numbers.Big_Integers; use Ada.Numerics.Big_Numbers.Big_Integers;

package Fibonacci_Squared is

   function Fib (N : Big_Natural) return Big_Natural is
      (if N < 2 then N else Fib (N-1) + Fib (N-2))
   with
     Annotate => (GNATprove, Terminating),
     Annotate => (GNATprove, False_Positive, "terminating annotation",
                  "That version of SPARK does not allow variant on Big_Natural");

   function Square_Fib (N : Big_Natural) return Big_Natural
   with
     Post => Square_Fib'Result = Fib (N) * Fib (N);

end Fibonacci_Squared;