proposition: Fact ex14 : forall z, generic_format r phi z -> generic_format r phi (- z).
proof: Proof. intros z; unfold generic_format, scaled_mantissa, cexp, F2R; simpl. todo. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)