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