proposition: Theorem Rnd_NG_pt_opp_inv : forall (F : R -> Prop) (P : R -> R -> Prop), ( forall x, F x -> F (-x) ) -> ( forall x f, P x f -> P (-x) (-f) ) -> forall x f : R, Rnd_NG_pt F P (-x) (-f) -> Rnd_NG_pt F P x f.
proof: Proof. intros F P HF HP x f (H1,H2). split. now apply Rnd_N_pt_opp_inv. destruct H2 as [H2|H2]. left. rewrite <- (Ropp_involutive x), <- (Ropp_involutive f). now apply HP. right. intros f2 Hxf2. rewrite <- (Ropp_involutive f). rewrite <- H2 with (-f2). apply sym_eq. apply Ropp_involutive. apply Rnd_N_pt_opp_inv. exact HF. now rewrite 2!Ropp_involutive. Qed.
imports: Coq(Reals) Raux Defs