Operator visibility question

[rod@praxis-cs.co.uk (Rod Chapman)]

Can anyone please tell me if the following code is legal?

package MT
is
   type T is range 0 .. 4;
end MT;

with MT;
--# inherit MT;
package VT
is
   function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
   A : constant := 2;
   B : constant MT.T := 3;

   C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
end VT;

The SPARK Examiner rejects the declaration of C with the message:

   9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
                                         ^
***        Semantic Error    :309: Operator not visible for these types.

On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
explain which is right, and (more importantly) why?
 Cheers,
  Rod Chapman
  SPARK Team
  Praxis Critical Systems