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