proposition: Theorem RND_Max_canonic : forall r : R, Fcanonic radix b (RND_Max r).
proof: Proof. intros r. unfold RND_Max in |- *; case (Rle_dec 0 r); intros H. apply RND_Max_Pos_canonic; auto. apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real. rewrite <- Ropp_0; apply Ropp_le_contravar; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz