proposition: Theorem EvenClosestRoundedModeP : RoundedModeP b radix EvenClosest.
proof: Proof. red in |- *; split. exact EvenClosestTotal. split. exact EvenClosestCompatible. split. exact EvenClosestMinOrMax. exact EvenClosestMonotone. Qed.
imports: Reals ZArith List PeanoNat Psatz