proposition: Theorem generic_format_abs_inv : forall x, generic_format (Rabs x) -> generic_format x.
proof: Proof. intros x. unfold generic_format, Rabs. case Rcase_abs ; intros _. rewrite scaled_mantissa_opp, cexp_opp, Ztrunc_opp. intros H. rewrite <- (Ropp_involutive x) at 1. rewrite H, F2R_Zopp. apply Ropp_involutive. easy. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop