Using .rlu files in SPARK Ada

[Ben Hocking <benjaminhocking@gmail.com>]

I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine.

I've been unable to satisfy the following check statement:
   a2 := x3 - x1;
   b := y3 - y1;
   --# check b < a2 -> (b rem a2 = b);

It generates the following VC:
y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1

In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have:
small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1].

(Note that I originally had:
small_rem: x rem y = x may_be_deduced_from [x < y].

However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.)

Am I doing something incorrectly, or is there some limitation of SPARK here?