proposition: Lemma Subexact: exists v:float, (FtoRradix v=x-y)%R /\ (Fbounded bo v) /\ (Fexp v=Z.min (Fexp x) (Fexp y))%Z.
proof: Proof. case (Req_dec (FtoRradix x) 0); intros. absurd (FtoRradix x =0)%R; auto with real. assert (~ is_Fzero x). apply FnormalNotZero with radix bo; auto. unfold is_Fzero in H0. unfold FtoRradix, FtoR; apply prod_neq_R0; auto with real zarith. apply IZR_neq; auto. apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. case (Rle_or_lt 0 y); intros S. exists (Fminus radix x y); split. unfold FtoRradix; rewrite Fminus_correct; auto with real zarith. split;[idtac|simpl; auto with zarith]. apply Sterbenz; auto with zarith; fold FtoRradix. elim Nx; auto. elim Ny; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoRradix y);[simpl; right; field; auto with real|idtac]. rewrite <- (Rabs_right y);[idtac|apply Rle_ge; auto]. rewrite <- (Rabs_right x). apply yLe2x; auto. elim dsd; intros I1 I2; apply Rle_ge; apply I1; auto. rewrite <- (Rabs_right y);[idtac|apply Rle_ge; auto]. rewrite <- (Rabs_right x). simpl; apply xLe2y; auto. elim dsd; intros I1 I2; apply Rle_ge; apply I1; auto. exists (Fopp (Fminus radix (Fopp x) (Fopp y))); split. unfold FtoRradix; rewrite Fopp_correct; rewrite Fminus_correct; auto with real zarith. rewrite Fopp_correct;rewrite Fopp_correct; ring. split;[idtac|simpl; auto with zarith]. apply oppBounded. apply Sterbenz; auto with zarith; fold FtoRradix. apply oppBounded; elim Nx; auto. apply oppBounded; elim Ny; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoRradix (Fopp y));[simpl; right; field; auto with real|idtac]. unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix. rewrite <- (Rabs_left1 y); auto with real. rewrite <- (Rabs_left1 x). apply yLe2x; auto. elim dsd; intros I1 I2; apply I2; auto with real. unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix. rewrite <- (Rabs_left1 y); auto with real. rewrite <- (Rabs_left1 x). simpl; apply xLe2y; auto. elim dsd; intros I1 I2; apply I2; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz