proposition: Theorem ClosestRoundedModeP : RoundedModeP b radix Closest.
proof: Proof. split; try exact ClosestTotal. split; try exact ClosestCompatible. split; try exact ClosestMinOrMax. try exact ClosestMonotone. Qed.
imports: Reals ZArith List PeanoNat Psatz