proposition: Theorem Rnd_N_pt_opp_inv : forall F : R -> Prop, ( forall x, F x -> F (- x) ) -> forall x f : R, Rnd_N_pt F (-x) (-f) -> Rnd_N_pt F x f.
proof: Proof. intros F HF x f (H1,H2). rewrite <- (Ropp_involutive f). repeat split. apply HF. apply H1. intros g H3. rewrite Ropp_involutive. replace (f - x)%R with (-(-f - -x))%R by ring. replace (g - x)%R with (-(-g - -x))%R by ring. rewrite 2!Rabs_Ropp. apply H2. now apply HF. Qed.
imports: Coq(Reals) Raux Defs