proposition: Theorem MaxRoundedModeP : RoundedModeP (isMax b radix).
proof: Proof. split; try red in |- *. intros r; apply MaxEx with (precision := precision); auto with zarith. split; try exact MaxCompatible. split; try apply MonotoneMax; red in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz