proposition: Lemma Zm: exists g : float beta, F2R g = m /\ canonical beta fexpe g /\ Z.even (Fnum g) = true.
proof: Proof. Proof with auto with typeclass_instances. case (d_ge_0); intros Y. destruct m_eq as (g,(Hg1,Hg2)); trivial. apply exists_even_fexp_lt. exists g; split; trivial. rewrite Hg2. rewrite mag_m; trivial. rewrite <- Fexp_d; trivial. rewrite Cd. unfold cexp. generalize (fexpe_fexp (mag beta (F2R d))). lia. destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. apply exists_even_fexp_lt. exists g; split; trivial. rewrite Hg2. rewrite mag_m_0; trivial. apply Z.le_lt_trans with (1:=fexpe_fexp _). generalize (fexp_m_eq_0 Y). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations