Need help understanding SPARK substitution rules

[Ben Hocking <benjaminhocking@gmail.com>]

I have the following math.ads:
========
package Math is
   function IsPositive (InVal : in Integer) return Boolean;
   --# return (InVal > 0);
   function IsNegative (InVal : in Integer) return Boolean;
   --# return (InVal < 0);
   function AlwaysTrue (InVal : in Integer) return Boolean;
   --# return True;
end Math;
========
and math.adb:
========
package body Math is
   function IsPositive (InVal : in Integer) return Boolean is
   begin
      return (InVal > 0);
   end IsPositive;

   function IsNegative (InVal : in Integer) return Boolean is
   begin
      return (InVal < 0);
   end IsNegative;

   function AlwaysTrue (InVal : in Integer) return Boolean is
   begin
      --# check not (InVal > 0) -> InVal <= 0;
      --# check not IsPositive(InVal) -> InVal <= 0;
      --# check not (InVal < 0) -> InVal >= 0;
      --# check not IsNegative(InVal) -> InVal >= 0;
      return (not IsPositive(InVal) or not IsNegative(InVal));
   end AlwaysTrue;
end Math;
========
The statement "check not (InVal > 0) -> InVal <= 0" is proven easily enough, but the next line ("check not IsPositive(InVal) -> InVal <= 0") is not, even though it's functionally equivalent. If I put the following line in math.rlu:
========
math_ispositive: ispositive(inval) may_be_replaced_by (inval > 0)
========
It now can prove it, and if I do the same thing with isnegative, the whole thing proves out (with the "return True" component being proven by ViCToR).

However, this seems like a very fragile way of assuring code correctness, so it reeks from "code smell". What is a better way of achieving this?

Thanks,
-Ben