proposition: Lemma mag_m: (0 < F2R d)%R -> (mag beta m =mag beta (F2R d) :>Z).
proof: Proof. Proof with auto with typeclass_instances. intros dPos; apply mag_unique_pos. split. apply Rle_trans with (F2R d). destruct (mag beta (F2R d)) as (e,He). simpl. rewrite Rabs_right in He. apply He. now apply Rgt_not_eq. apply Rle_ge; now left. apply d_le_m. case m_le_u; intros H. apply Rlt_le_trans with (1:=H). rewrite u_eq. apply round_le_generic... apply generic_format_bpow. apply valid_exp. apply mag_generic_gt... now apply Rgt_not_eq. now apply generic_format_canonical. case (Rle_or_lt x (bpow (mag beta (F2R d)))); trivial; intros Z. absurd ((bpow (mag beta (F2R d)) <= (F2R d)))%R. apply Rlt_not_le. destruct (mag beta (F2R d)) as (e,He). simpl in *; rewrite Rabs_right in He. apply He. now apply Rgt_not_eq. apply Rle_ge; now left. apply Rle_trans with (round beta fexp Zfloor x). 2: right; apply sym_eq, d_eq. apply round_ge_generic... apply generic_format_bpow. apply valid_exp. apply mag_generic_gt... now apply Rgt_not_eq. now apply generic_format_canonical. now left. replace m with (F2R d). destruct (mag beta (F2R d)) as (e,He). simpl in *; rewrite Rabs_right in He. apply He. now apply Rgt_not_eq. apply Rle_ge; now left. unfold m in H |- *. lra. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations