proposition: Theorem Fmul_aux_correct : forall beta (x y : float beta), UtoX (Fmul_aux x y) = Xmul (FtoX x) (FtoX y).
proof: Proof. intros beta [ | | sx mx ex ] [ | | sy my ey ] ; simpl ; try apply refl_equal. rewrite Rmult_0_l. apply refl_equal. rewrite Rmult_0_l. apply refl_equal. rewrite Rmult_0_r. apply refl_equal. rewrite FtoR_mul. apply refl_equal. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic