proposition: Lemma m_eq : (0 < F2R d)%R -> exists f:float beta, F2R f = m /\ (Fexp f = fexp (mag beta x) - 1)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros Y. specialize (Zeven_ex (radix_val beta)); rewrite Even_beta. intros (b, Hb); rewrite Zplus_0_r in Hb. destruct u'_eq as (u', (Hu'1,Hu'2)); trivial. exists (Fmult (Float beta b (-1)) (Fplus d u'))%R. split. rewrite F2R_mult, F2R_plus, Hu'1. unfold m; rewrite Rmult_comm. unfold Rdiv; apply f_equal. unfold F2R; simpl; unfold Z.pow_pos; simpl. rewrite Zmult_1_r, Hb, mult_IZR. simpl; field. apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). rewrite Rmult_0_r, <- (mult_IZR 2), <-Hb. apply radix_pos. apply trans_eq with (-1+Fexp (Fplus d u'))%Z. unfold Fmult. destruct (Fplus d u'); reflexivity. rewrite Zplus_comm; unfold Zminus; apply f_equal2. 2: reflexivity. rewrite Fexp_Fplus. rewrite Z.min_l. now rewrite Fexp_d. rewrite Hu'2; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations