proposition: Theorem mult_correct : forall x y : float beta, round beta fexp rnd (F2R x * F2R y) = F2R (mult x y).
proof: Proof. intros x y. unfold mult. rewrite <- F2R_mult. destruct (Fmult x y) as [m e]. rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact). 3: now right. destruct truncate as [[m' e'] l']. apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))). apply Rsgn_F2R. apply inbetween_Exact. apply sym_eq, F2R_Zabs. Qed.
imports: Coq(ZArith Reals) Flocq(Core Bracket Round Operations Div Sqrt)