proposition: Theorem generic_format_canonical : forall f, canonical f -> generic_format (F2R f).
proof: Proof. intros (m, e) Hf. unfold canonical in Hf. simpl in Hf. unfold generic_format, scaled_mantissa. rewrite <- Hf. apply F2R_eq. 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