proposition: Theorem Rnd_DN_opp : forall F : R -> Prop, ( forall x, F x -> F (- x) ) -> forall rnd1 rnd2 : R -> R, Rnd_DN F rnd1 -> Rnd_UP F rnd2 -> forall x, rnd1 (- x) = - rnd2 x.
proof: Proof. intros F HF rnd1 rnd2 H1 H2 x. rewrite <- (Ropp_involutive (rnd1 (-x))). apply f_equal. apply (Rnd_UP_unique F (fun x => - rnd1 (-x))) ; trivial. intros y. pattern y at 1 ; rewrite <- Ropp_involutive. apply Rnd_UP_pt_opp. apply HF. apply H1. Qed.
imports: Coq(Reals) Raux Defs