proposition: Lemma exists_even_fexp_lt: forall (c:Z->Z), forall (x:R), (exists f:float beta, F2R f = x /\ (c (mag beta x) < Fexp f)%Z) -> exists f:float beta, F2R f =x /\ canonical beta c f /\ Z.even (Fnum f) = true.
proof: Proof. Proof with auto with typeclass_instances. intros c x (g,(Hg1,Hg2)). exists (Float beta (Fnum g*Z.pow (radix_val beta) (Fexp g - c (mag beta x))) (c (mag beta x))). assert (F2R (Float beta (Fnum g*Z.pow (radix_val beta) (Fexp g - c (mag beta x))) (c (mag beta x))) = x). unfold F2R; simpl. rewrite mult_IZR, IZR_Zpower. rewrite Rmult_assoc, <- bpow_plus. rewrite <- Hg1; unfold F2R. apply f_equal, f_equal. ring. lia. split; trivial. split. unfold canonical, cexp. now rewrite H. simpl. rewrite Z.even_mul. rewrite Z.even_pow. rewrite Even_beta. apply Bool.orb_true_intro. now right. lia. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations