proposition: Fact ex14 : forall z, generic_format r phi z -> generic_format r phi (- z).
proof: Proof. intros z Gz. destruct (Req_dec z 0) as [zZ|zNZ]. rewrite zZ in *; rewrite Ropp_0; auto. unfold generic_format, F2R, scaled_mantissa, cexp; simpl. rewrite ex13; auto. assert (H :- z * bpow r (- phi (mag r z)) = - (z * bpow r (- phi (mag r z)))) by ring. rewrite H, Ztrunc_opp, opp_IZR. unfold generic_format, F2R, scaled_mantissa, cexp in Gz; simpl in Gz. lra. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)