proposition: Theorem MinRoundedModeP : RoundedModeP (isMin b radix).
proof: Proof. split; try red in |- *. intros r; apply MinEx with (precision := precision); auto with zarith. split; try exact MinCompatible. split; try apply MonotoneMin; red in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz