proposition: Theorem F2R_mult : forall f1 f2 : float beta, F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R.
proof: Proof. intros (m1, e1) (m2, e2). unfold Fmult, F2R. simpl. rewrite mult_IZR, bpow_plus. ring. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop