proposition: Theorem generic_format_abs : forall x, generic_format x -> generic_format (Rabs x).
proof: Proof. intros x Hx. unfold generic_format. rewrite scaled_mantissa_abs, cexp_abs. rewrite Ztrunc_abs. rewrite F2R_Zabs. now apply f_equal. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop