proposition: Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta, F2R f = m /\ (Fexp f = fexp (mag beta (F2R u)) -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. exists (Fmult (Float beta b (-1)) u)%R. split. rewrite F2R_mult; unfold m; rewrite <- Y, Rplus_0_l. 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 u)%Z. unfold Fmult. destruct u; reflexivity. rewrite Zplus_comm, Cu; unfold Zminus; now apply f_equal2. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations