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