proposition: Theorem scaled_mantissa_opp : forall x, scaled_mantissa (-x) = (-scaled_mantissa x)%R.
proof: Proof. intros x. unfold scaled_mantissa. rewrite cexp_opp. now rewrite Ropp_mult_distr_l_reverse. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop