Exact rational bound arithmetic

This scoped instance uses exact rational operations for both directed endpoints. Its real interpretation laws are proved in NN.Verification.Cert.RationalReflection.

@[instance_reducible]

def Spec.RationalAlgebraic.instBoundOpsRat : NN.MLTheory.CROWN.BoundOps ℚ

Rational certificate arithmetic is exact, including affine reassociation.