proposition: Theorem Rnd_odd_pt_opp_inv : forall x f : R, Rnd_odd_pt (-x) (-f) -> Rnd_odd_pt x f.
proof: Proof. Proof with auto with typeclass_instances. intros x f (H1,H2). split. replace f with (-(-f))%R by ring. now apply generic_format_opp. destruct H2. left. replace f with (-(-f))%R by ring. rewrite H; ring. right. destruct H as (H2,(g,(Hg1,(Hg2,Hg3)))). split. destruct H2. right. replace f with (-(-f))%R by ring. replace x with (-(-x))%R by ring. apply Rnd_UP_pt_opp... apply generic_format_opp. left. replace f with (-(-f))%R by ring. replace x with (-(-x))%R by ring. apply Rnd_DN_pt_opp... apply generic_format_opp. exists (Float beta (-Fnum g) (Fexp g)). split. rewrite F2R_Zopp. replace f with (-(-f))%R by ring. rewrite Hg1; reflexivity. split. now apply canonical_opp. simpl. now rewrite Z.even_opp. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations