proposition: Theorem scaled_mantissa_generic : forall x, generic_format x -> scaled_mantissa x = IZR (Ztrunc (scaled_mantissa x)).
proof: Proof. intros x Hx. unfold scaled_mantissa. pattern x at 1 3 ; rewrite Hx. unfold F2R. simpl. rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. now rewrite Ztrunc_IZR. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop