proposition: Lemma scale2_correct : forall x d, sensible_format = true -> toX (scale2 x d) = Xmul (toX x) (Xreal (bpow radix2 (StoZ d))).
proof: Proof. intros [|m e] d H. easy. unfold toX. simpl. generalize (mantissa_sign_correct m). case_eq (mantissa_sign m). intros Hs _. simpl. rewrite Hs. now rewrite Rmult_0_l. intros s m' _ (Em,Vm). simpl. generalize (mantissa_scale2_correct m' d Vm). case mantissa_scale2. intros p e' (Ep, Vp). rewrite toF_float with (1 := Vp). rewrite exponent_add_correct. simpl. rewrite 2!FtoR_split. unfold Defs.F2R. simpl. rewrite Rmult_assoc, (Rmult_comm (bpow radix (EtoZ e))). rewrite 2!IZR_cond_Zopp, <- 2!cond_Ropp_mult_l. apply (f_equal (fun v => Xreal (cond_Ropp s v))). rewrite Zplus_comm, bpow_plus, <- 2!Rmult_assoc. unfold radix. now rewrite Ep. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig