proposition: Theorem RND_Max_correct : forall r : R, isMax b radix r (RND_Max r).
proof: Proof. intros r. unfold RND_Max in |- *; case (Rle_dec 0 r); intros H. apply RND_Max_Pos_correct; auto. pattern r at 1 in |- *; rewrite <- (Ropp_involutive r). apply MinOppMax; apply RND_Min_Pos_correct; auto with real. rewrite <- Ropp_0; apply Ropp_le_contravar; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz