proposition: Fact ex3 x : FIX_format r e x -> FIX_format r e (- x).
proof: Proof. intros [f fE fExp]. exists {| Fnum := - Fnum f; Fexp := Fexp f |}. - rewrite fE; unfold F2R; simpl; rewrite opp_IZR; ring. - auto. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)