proposition: Theorem Rnd_DN_pt_opp : forall F : R -> Prop, ( forall x, F x -> F (- x) ) -> forall x f : R, Rnd_UP_pt F x f -> Rnd_DN_pt F (-x) (-f).
proof: Proof. intros F HF x f H. repeat split. apply HF. apply H. apply Ropp_le_contravar. apply H. intros g Hg. rewrite <- (Ropp_involutive g). intros Hxg. apply Ropp_le_contravar. apply H. now apply HF. now apply Ropp_le_cancel. Qed.
imports: Coq(Reals) Raux Defs