proposition: Theorem exp_fast_correct : forall prec x, contains (I.convert (exp_fast prec x)) (Xexp (F.toX x)).
proof: Proof. intros prec x. unfold exp_fast. rewrite F'.cmp_correct, F.zero_correct. case_eq (F.toX x). easy. intros r Hr. simpl. case Rcompare_spec ; intros H. replace r with (Ropp (toR (F.neg x))). apply expn_reduce_correct. unfold toR. now rewrite F'.neg_correct, Hr. unfold toR. rewrite F'.neg_correct, Hr. rewrite <- Ropp_0. now apply Ropp_lt_contravar. unfold toR. rewrite F'.neg_correct, Hr. apply Ropp_involutive. rewrite H, exp_0. now apply I.fromZ_small_correct. generalize (F.incr_prec prec 1). clear prec. intro prec. case_eq (I.invnz prec (expn_reduce prec x)) ; intros. unfold c1. rewrite I.bnd_correct. 2: apply I.valid_lb_real ; now rewrite F.fromZ_correct. 2: now apply I.valid_ub_nan. split. rewrite F.fromZ_correct by easy. simpl. rewrite <- exp_0. apply Rlt_le. now apply exp_increasing. now rewrite F'.nan_correct. rewrite <- H0. rewrite <- (Ropp_involutive r). rewrite exp_Ropp. replace (Xreal (/ exp (- r))) with (Xinv (Xreal (exp (- toR x)))). apply I.invnz_correct. { intros H1. injection H1. apply Rgt_not_eq. apply exp_pos. } apply expn_reduce_correct. unfold toR. now rewrite Hr. unfold toR. now rewrite Hr. unfold toR. rewrite Hr. unfold Xinv'. simpl. case is_zero_spec ; intro H1. elim Rgt_not_eq with (2 := H1). apply exp_pos. apply refl_equal. Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float