proposition: Theorem scaled_mantissa_abs : forall x, scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).
proof: Proof. intros x. unfold scaled_mantissa. rewrite cexp_abs, Rabs_mult. apply f_equal. apply sym_eq. apply Rabs_pos_eq. apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop