Solver for Linear Inequalities
Signature
> : rational -> rational -> type.
>= : rational -> rational -> type.
+> : {Z:rational} X > Y -> (X + Z) > (Y + Z).
+>= : {Z:rational} X >= Y -> (X + Z) >= (Y + Z).
>>= : X > Y -> X >= Y.
0>=0 : 0 >= 0.
Special constants
qɬ : q > 0. (for all positive rationals q)