proposition: Lemma mag_correct : forall f, (Rabs (toR f) < bpow radix (StoZ (mag f)))%R.
proof: Proof. intros f. unfold StoZ, mag. destruct f as [ |sm e]. { change (toR Fnan) with 0%R. rewrite Rabs_R0. apply bpow_gt_0. } unfold toR, toX. simpl. generalize (mantissa_sign_correct sm). destruct mantissa_sign as [ |s m]. { intros _. change (proj_val (FtoX Fzero)) with 0%R. rewrite Rabs_R0. apply bpow_gt_0. } simpl. intros H. rewrite FtoR_split. rewrite exponent_add_correct. rewrite mantissa_digits_correct by apply H. rewrite <- digits_conversion, Zplus_comm. apply Rlt_le_trans with (1 := bpow_mag_gt radix _). apply bpow_le, Z.eq_le_incl. rewrite <- Raux.mag_abs, <- Float_prop.F2R_Zabs, abs_cond_Zopp. now apply Float_prop.mag_F2R_Zdigits. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig