proposition: Theorem generic_format_opp : forall x, generic_format x -> generic_format (-x).
proof: Proof. intros x Hx. unfold generic_format. rewrite scaled_mantissa_opp, cexp_opp. rewrite Ztrunc_opp. rewrite F2R_Zopp. now apply f_equal. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop