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